lib/scripts/download_file
author wenzelm
Wed, 11 Dec 2024 11:18:52 +0100
changeset 81579 cf4bebd770b5
parent 80213 d13b8ee54885
permissions -rw-r--r--
proper bundle binomial_syntax; NB: precedence of "choose" changes silently from 65 to 64 in 200107cdd3ac, but old 65 was still seen in the wild;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77053
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     1
# -*- shell-script -*- :mode=shellscript:
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     2
#
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     3
# Bash function to download file via "curl".
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     4
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     5
function download_file ()
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     6
{
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     7
  [ "$#" -ne 2 ] && {
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     8
    echo "Bad arguments for download_file" >&2
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
     9
    return 2
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    10
  }
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    11
  local REMOTE="$1"
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    12
  local LOCAL="$2"
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    13
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    14
  type -p curl > /dev/null || {
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    15
    echo "Require \"curl\" to download files" >&2
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    16
    return 2
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    17
  }
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    18
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    19
  echo "Getting \"$REMOTE\""
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    20
  mkdir -p "$(dirname "$LOCAL")"
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    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
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    23
  then
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    24
    mv -f "${LOCAL}.part" "$LOCAL"
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    25
  else
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    26
    rm -f "${LOCAL}.part"
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    27
    echo "Failed to download \"$REMOTE\"" >&2
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    28
    return 2
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    29
  fi
c839b84ee66f more modular shell script;
wenzelm
parents:
diff changeset
    30
}