aboutsummaryrefslogtreecommitdiff
path: root/reproduce/src/make
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 /reproduce/src/make
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 'reproduce/src/make')
0 files changed, 0 insertions, 0 deletions