Get a file from an URL (wget, curl)

wget_curl_file.sh

#!/bin/bash

wget_curl_file() { # Args: from_URL, to_file.  Optional arg: Log.
  local log='' ;
  log=$3 ;
  [[ $log ]] || log=`mktemp "${TMPDIR:-/tmp}/tmp.XXXXXXXXXX"` ;
  { wget -qO $2 $1 2>$log || curl -s $1 > $2 ; } &> $log ;
  local e=$?
  [[ $e -eq 0 ]] || {
    echo "ERROR: $e from wget or curl:" 1>&2
    local sets=$-
    set -x
    tail $log 1>&2
    set +x
    set $sets
    echo "  (For more, see '$log'.)" 1>&2
  }
  return $e
}

#