aboutsummaryrefslogtreecommitdiff
path: root/configure
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2018-11-22 12:17:32 +0000
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2018-11-22 12:17:32 +0000
commit311572e0c1375429de998d70eb7d587d7b8032c4 (patch)
tree677736168f819231aa8034b3909985a5ae2b4424 /configure
parente3ba3642a87cce8b001c8d2a81d0f2118866ba30 (diff)
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.
Diffstat (limited to 'configure')
-rwxr-xr-xconfigure5
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