From 311572e0c1375429de998d70eb7d587d7b8032c4 Mon Sep 17 00:00:00 2001 From: Mohammad Akhlaghi Date: Thu, 22 Nov 2018 12:17:32 +0000 Subject: Wget not using server timestamps By default, Wget uses the same time stamp for the downloaded file as the server. As a result, if a dependency was previously built before the tarball was uploaded to the server, the pipeline wouldn't recognize that its new and wouldn't re-build it. With this commit, we are adding the `--no-use-server-timestamps' to the call to Wget to fix this problem. I also noticed that (probably as a bug left over from the time we were testing the configure script), we were manually setting the `userread' variable to `n' independent of what the user provided. This has also been fixed. --- configure | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/configure b/configure index de42d3f..37a5224 100755 --- a/configure +++ b/configure @@ -148,7 +148,6 @@ if [ -f $pconf ] || [ -f $glconf ]; then do read -p"Re-write existing configuration file(s) (y/n)? " userread done - userread=n # Set `rewriteconfig'. if [ $userread = "n" ]; then @@ -180,7 +179,7 @@ fi # the web address. if [ $rewritepconfig = yes ]; then if type wget > /dev/null 2>/dev/null; then - downloader="wget -O"; + downloader="wget --no-use-server-timestamps -O"; else cat <