aboutsummaryrefslogtreecommitdiff
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
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.
-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)