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.

1 files 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 <<EOF
 
@@ -496,7 +495,7 @@ make -f reproduce/src/make/dependencies-basic.mk \
 # script. Bash and Make were the tools we need to run Makefiles, so we had
 # to build them in this script. But after this, we can rely on Makefiles.
 numthreads=$($instdir/bin/nproc)
-./.local/bin/make -f reproduce/src/make/dependencies.mk \
+./.local/bin/make -f reproduce/src/make/dependencies.mk    \
                   static_build=$static_build -j$numthreads