diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2025-02-17 15:21:26 +0100 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2025-02-17 15:21:26 +0100 |
| commit | 78b28fd5f986cb334008cdfbc2b7b3aa6e0d53de (patch) | |
| tree | 5e9727cb31b8e73f8f3fa6c35db0ed4ae5744405 /reproduce/analysis/bash | |
| parent | 27d758a8f479c300466f650cde68c63d42deb6db (diff) | |
| parent | a55a407c1f2a1b280be78f24abd1fe6d4a8032e2 (diff) | |
Configuration: Imported recent updates from Maneageaas-journals
Until this commit, the AAS journals branch was based on Maneage commit
8161194 (dated 2022-05-22). However, maneage has been updated recently so
it is necessary to also update this branch.
With this commit, the merge has been done (and tested).
Diffstat (limited to 'reproduce/analysis/bash')
| -rwxr-xr-x | reproduce/analysis/bash/download-multi-try.sh (renamed from reproduce/analysis/bash/download-multi-try) | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/reproduce/analysis/bash/download-multi-try b/reproduce/analysis/bash/download-multi-try.sh index d7e9be2..bea88d5 100755 --- a/reproduce/analysis/bash/download-multi-try +++ b/reproduce/analysis/bash/download-multi-try.sh @@ -1,14 +1,19 @@ -#!/bin/sh +#!/usr/bin/env sh # # Attempt downloading multiple times before crashing whole project. From # the top project directory (for the shebang above), this script must be # run like this: # -# $ /path/to/download-multi-try downloader lockfile input-url downloaded-name +# $ $SHELL /path/to/download-multi-try.sh downloader lockfile \ +# input-url downloaded-name # -# NOTE: The 'downloader' must contain the option to specify the output name -# in its end. For example "wget -O". Any other option can also be placed in -# the middle. +# NOTE: +# - This script doesn't have a Shebang because in different stages it +# should be built with different shells ('/bin/sh' before Maneage +# installs its own shell and afterwards with Maneage's own shell). +# - The 'downloader' must contain the option to specify the output name +# in its end. For example "wget -O". Any other option can also be placed in +# the middle. # # Due to temporary network problems, a download may fail suddenly, but # succeed in a second try a few seconds later. Without this script that @@ -26,7 +31,7 @@ # reason, you don't want to use a lock file, set the 'lockfile' name to # 'nolock'. # -# Copyright (C) 2019-2023 Mohammad Akhlaghi <mohammad@akhlaghi.org> +# Copyright (C) 2019-2025 Mohammad Akhlaghi <mohammad@akhlaghi.org> # # This program is free software: you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by |