diff options
author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2022-05-09 13:32:47 +0200 |
---|---|---|
committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2022-05-09 23:52:29 +0200 |
commit | 9fdeebaacd06d57c479cd69e9937c4bfe5d0a286 (patch) | |
tree | 012e6194ad6e25a81a9c99b4d0bd0852bc9a12af /reproduce/analysis/bash | |
parent | 480184b3da399fab11b50e67f01d2efa6bea0e3e (diff) | |
parent | f51b5e2e500dd6450a5a3425e85df78245fc5c5c (diff) |
Imported recent updates in Maneage, conflicts fixed
Until now, Maneage had undergone some updates.
With this commit, those updates have been imported and the conflicts that
resulted were fixed. They were all cosmetic and had no effect on the
analysis. The most significant one was about the change in the format of
'INPUTS.conf'.
In the process, I also noticed that the IEEEtran LaTeX package is now
called 'ieeetran' (the 'tlmgr' of TeXLive 2022 was failing).
Diffstat (limited to 'reproduce/analysis/bash')
-rwxr-xr-x | reproduce/analysis/bash/download-multi-try | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/reproduce/analysis/bash/download-multi-try b/reproduce/analysis/bash/download-multi-try index 76eb859..994a8fa 100755 --- a/reproduce/analysis/bash/download-multi-try +++ b/reproduce/analysis/bash/download-multi-try @@ -6,7 +6,7 @@ # # $ /path/to/download-multi-try downloader lockfile input-url downloaded-name # -# NOTE: The `downloader' must contain the option to specify the output 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. # @@ -20,13 +20,13 @@ # world, downloading is done much faster in serial, not in parallel. But # the project's processing may be done in parallel (with multiple threads # needing to download different files at the same time). Therefore, this -# script uses the `flock' program to only do one download at a time. To +# script uses the 'flock' program to only do one download at a time. To # benefit from it, any call to this script must be given the same lock # file. If your system has multiple ports to the internet, or for any -# reason, you don't want to use a lock file, set the `lockfile' name to -# `nolock'. +# reason, you don't want to use a lock file, set the 'lockfile' name to +# 'nolock'. # -# Copyright (C) 2019-2021 Mohammad Akhlaghi <mohammad@akhlaghi.org> +# Copyright (C) 2019-2022 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 @@ -114,9 +114,9 @@ while [ ! -f "$outname" ]; do sleep $tstep fi - # Attempt downloading the file. Note that the `downloader' ends with + # Attempt downloading the file. Note that the 'downloader' ends with # the respective option to specify the output name. For example "wget - # -O" (so `outname', that comes after it) will be the name of the + # -O" (so 'outname', that comes after it) will be the name of the # downloaded file. if [ x"$lockfile" = xnolock ]; then if ! $downloader $outname $inurl; then rm -f $outname; fi |