diff options
| -rw-r--r-- | .file-metadata | bin | 4007 -> 4007 bytes | |||
| -rwxr-xr-x | reproduce/src/bash/download-multi-try | 6 |
2 files changed, 3 insertions, 3 deletions
diff --git a/.file-metadata b/.file-metadata Binary files differindex c36f801..ebc3dfe 100644 --- a/.file-metadata +++ b/.file-metadata diff --git a/reproduce/src/bash/download-multi-try b/reproduce/src/bash/download-multi-try index 642908e..1be2ffa 100755 --- a/reproduce/src/bash/download-multi-try +++ b/reproduce/src/bash/download-multi-try @@ -1,10 +1,10 @@ #!.local/bin/bash # # Attempt downloading multiple times before crashing whole pipeline. From -# the top paper directory (for the shebang above), this script must be run -# like this: +# the top project directory (for the shebang above), this script must be +# run like this: # -# $ ./download-multi-try downloader lockfile input-url downloaded-name +# $ /path/to/download-multi-try downloader lockfile input-url downloaded-name # # Due to temporary network problems, a download may fail suddenly, but # succeed in a second try a few seconds later. Without this script that |