From: Wolfgang Bangerth Date: Sun, 20 May 2018 08:27:08 +0000 (+0800) Subject: Use wget instead of curl. X-Git-Tag: v9.1.0-rc1~1123^2 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c4fc68cba0ccf892ee0d7bc2b7515c4a7fbddad9;p=dealii.git Use wget instead of curl. Also show a progress bar for the download, but be otherwise quiet. --- diff --git a/contrib/utilities/download_clang_format b/contrib/utilities/download_clang_format index 0a0f921b45..a739561847 100755 --- a/contrib/utilities/download_clang_format +++ b/contrib/utilities/download_clang_format @@ -59,13 +59,25 @@ then exit 1 fi -echo "Downloading and installing clang-format-6." +echo "Downloading and installing clang-format-6 from ${URL}/${FILENAME}" mkdir "${CLANG_PATH}" tmpdir="${TMPDIR:-/tmp}/dealiiclang${RANDOM}${RANDOM}" mkdir -p "${tmpdir}" cd "${tmpdir}" -curl -s -L "${URL}/${FILENAME}" -O > /dev/null +if [ -x "$(command -v wget)" ]; then + echo "Using wget to download..." + wget -q --show-progress -L "${URL}/${FILENAME}" > /dev/null +else + if [ -x "$(command -v curl)" ]; then + echo "Using curl to download..." + curl -s -L "${URL}/${FILENAME}" -O > /dev/null + else + echo "Error: Neither wget nor curl is available..." + exit 1 + fi +fi + if echo "${CHECKSUM}" | "${CHECKSUM_CMD}" -c; then tar xfz "${FILENAME}" -C "${PRG}" > /dev/null else