From e5082a353ead04ec735cfd1c9e60e4fda87da922 Mon Sep 17 00:00:00 2001 From: Mohammad Akhlaghi Date: Fri, 30 Nov 2018 17:02:46 +0000 Subject: 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. --- configure | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'configure') 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 < /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 -- cgit v1.2.1