aboutsummaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2018-12-05 11:35:53 +0000
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2018-12-05 11:35:53 +0000
commit3ddbaa75483f0fc14ad2840f6aa1478ad2c1b902 (patch)
tree5d4919279a3c830a0a96ccf37380d2482e696aca /configure
parent109d8ec7be460ef0fd708ebd118e45edeb445256 (diff)
Corrected comment on downloader in configure script
The comment above the downloader section of the configure script was not up to date with how the pipeline uses a downloader during configuration and building now. So it was updated.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure17
1 files changed, 5 insertions, 12 deletions
diff --git a/configure b/configure
index 32be0ae..28291c3 100755
--- a/configure
+++ b/configure
@@ -166,18 +166,11 @@ fi
# Identify the downloader tool
# ----------------------------
#
-# We use Wget for the downloading. As of November 12th, cURL couldn't
-# download Ghostscript's source from its standard address, but Wget
-# could. Until November 12th, we would check for cURL or Wget, so we
-# defined this check system here (explained in the next paragraph of this
-# comment). For now its redundant, but if the fix for cURL is found later,
-# we can add it back (or add other downloaders). So we'll keep it.
-#
-# Since the options specifying the output filename are different between
-# the two, we'll also specify the output option within the `downloader'
-# variable. So it is important to first give the output filename after
-# calling `DOWNLOADER' within the Makefiles, and finish the command with
-# the web address.
+# After this `./configure' script finishes, we will have both Wget and cURL
+# for downloading any necessary dataset during the processing. However, to
+# complete the configuration, we may also need to download the source code
+# of some necessary software packages (including the downloaders). So we
+# need to check the host's available tool for downloading at this step.
if [ $rewritepconfig = yes ]; then
if type wget > /dev/null 2>/dev/null; then
name=$(which wget)