diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-22 12:17:32 +0000 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2018-11-22 12:17:32 +0000 |
commit | 311572e0c1375429de998d70eb7d587d7b8032c4 (patch) | |
tree | 677736168f819231aa8034b3909985a5ae2b4424 /README-pipeline.md | |
parent | e3ba3642a87cce8b001c8d2a81d0f2118866ba30 (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 'README-pipeline.md')
0 files changed, 0 insertions, 0 deletions