aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorMohammad Akhlaghi <mohammad@akhlaghi.org>2020-02-11 00:38:11 +0100
committerMohammad Akhlaghi <mohammad@akhlaghi.org>2020-02-11 00:38:11 +0100
commit6d68865a5d083b8892c3f4854284bb2036f1efdf (patch)
tree1eb2874d93efc7ba0ec16d4528d241a6a340122a /.gitignore
parent24be94568eeaeb5c51071687070a4c0ffa06a1ef (diff)
Using backup server when original download server fails
Until now, the main download script could only check one server for the given URL. However, ultimately the actual server that a file is downloaded from is irrelevant for this project: we actually check its checksum. Especially in the case of software (which are distributed over many servers), this can usually be very annoying: the servers may not properly communicate with the running system and even the 10 trials won't be enough. With this commit, the download script `reproduce/analysis/bash/download-multi-try' can take a new optional argument (a 5th argument). It assumes this argument is a space-separated list of server(s) to use as backup for the original URL. When downloading from the original URL fails, it will look into this list and try downloading the same file from each given server.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions