From: Wolfgang Bangerth <bangerth@colostate.edu>
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