author | wenzelm |
Wed, 11 Dec 2024 11:18:52 +0100 | |
changeset 81579 | cf4bebd770b5 |
parent 80213 | d13b8ee54885 |
permissions | -rw-r--r-- |
77053 | 1 |
# -*- shell-script -*- :mode=shellscript: |
2 |
# |
|
3 |
# Bash function to download file via "curl". |
|
4 |
||
5 |
function download_file () |
|
6 |
{ |
|
7 |
[ "$#" -ne 2 ] && { |
|
8 |
echo "Bad arguments for download_file" >&2 |
|
9 |
return 2 |
|
10 |
} |
|
11 |
local REMOTE="$1" |
|
12 |
local LOCAL="$2" |
|
13 |
||
14 |
type -p curl > /dev/null || { |
|
15 |
echo "Require \"curl\" to download files" >&2 |
|
16 |
return 2 |
|
17 |
} |
|
18 |
||
19 |
echo "Getting \"$REMOTE\"" |
|
20 |
mkdir -p "$(dirname "$LOCAL")" |
|
21 |
||
80213
d13b8ee54885
obsolete: macOS 10.x is no longer supported (see also 059743bc8311);
wenzelm
parents:
77053
diff
changeset
|
22 |
if curl --fail --silent --location "$REMOTE" > "${LOCAL}.part" |
77053 | 23 |
then |
24 |
mv -f "${LOCAL}.part" "$LOCAL" |
|
25 |
else |
|
26 |
rm -f "${LOCAL}.part" |
|
27 |
echo "Failed to download \"$REMOTE\"" >&2 |
|
28 |
return 2 |
|
29 |
fi |
|
30 |
} |