cURL now also available as downloader with -L flag

The main reason I wasn't using cURL as a downloading tool was that I wasn't
familar with how to ask it to follow a re-direct. But I just found out that
its with the `-L' configure time option. So it is now added as a downloader
tool to the pipeline.

1 files changed, 13 insertions, 4 deletions

diff --git a/configure b/configure
index 840a350..b39d825 100755
--- a/configure
+++ b/configure
@@ -180,8 +180,17 @@ fi
 # the web address.
 if [ $rewritepconfig = yes ]; then
     if type wget > /dev/null 2>/dev/null; then
-        wgetname=$(which wget)
-        downloader="$wgetname --no-use-server-timestamps -O";
+        name=$(which wget)
+
+        # By default Wget keeps the remote file's timestamp, so we'll have
+        # to disable it manually.
+        downloader="$name --no-use-server-timestamps -O";
+    elif type curl > /dev/null 2>/dev/null; then
+        name=$(which curl)
+
+        # - cURL doesn't keep the remote file's timestamp by default.
+        # - With the `-L' option, we tell cURL to follow redirects.
+        downloader="$name -L -o"
     else
         cat <<EOF
 
@@ -591,8 +600,8 @@ fi
 # some versions of Make complain about not having enough 'pipe' (memory) on
 # some systems. After some searching, I found out its because of too many
 # threads.
-if which nproc &> /dev/null; then numthreads=$(nproc --all);
-else                              numthreads=2;
+if which nproc > /dev/null 2>/dev/null; then numthreads=$(nproc --all);
+else                                         numthreads=2;
 fi
 make -f reproduce/src/make/dependencies-basic.mk \
      static_build=$static_build -j$numthreads