diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-02-06 18:08:19 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2019-02-06 18:08:19 +0000 |
| commit | 1c508e636b90ae170213ccf71771711156dd8f52 (patch) | |
| tree | 0e9c6e306fc231a92497275d621e21d53737ad48 /.file-metadata | |
| parent | 33e00f02d4ecd28ea5084fc553d2ad182a11ca52 (diff) | |
Wrapper script for multiple attempts at downloading inputs
Until now, downloading was treated similar to any other operation in the
Makefile: if it crashes, the pipeline would crash. But network errors
aren't like processing errors: attempting to download a second time will
probably not crash (network relays are very complex and not reproducible
and packages get lost all the time)!
This is usually not felt in downloading one or two files, but when
downloading many thousands of files, it will happen every once and a while
and its a real waste of time until you check to just press enter again!
With this commit we have the `reproduce/src/bash/download-multi-try.sh'
script in the pipeline which will repeat the downoad several times (with
incrasing time intervals) before crashing and thus fix the problem.
Diffstat (limited to '.file-metadata')
| -rw-r--r-- | .file-metadata | bin | 3843 -> 4010 bytes |
1 files changed, 0 insertions, 0 deletions
diff --git a/.file-metadata b/.file-metadata Binary files differindex fe72296..e1cbf37 100644 --- a/.file-metadata +++ b/.file-metadata |