From: Daniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Date: Wed, 23 May 2018 11:35:21 +0000 (+0200)
Subject: Only use progress bar in wget if available
X-Git-Tag: v9.1.0-rc1~1109^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=16374b2b385bfc6d26d9c957b2c210e6d83d74ca;p=dealii.git

Only use progress bar in wget if available
---

diff --git a/contrib/utilities/download_clang_format b/contrib/utilities/download_clang_format
index a739561847..d02752266c 100755
--- a/contrib/utilities/download_clang_format
+++ b/contrib/utilities/download_clang_format
@@ -67,11 +67,15 @@ mkdir -p "${tmpdir}"
 cd "${tmpdir}"
 if [ -x "$(command -v wget)" ]; then
   echo "Using wget to download..."
-  wget -q --show-progress -L "${URL}/${FILENAME}" > /dev/null
+  # set progress option if available
+  wget --help | grep -q '\--show-progress' && \
+        _PROGRESS_OPT="--show-progress" || _PROGRESS_OPT=""
+
+  wget -q $_PROGRESS_OPT -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
+    curl --progress-bar -L "${URL}/${FILENAME}" -O > /dev/null
   else
     echo "Error: Neither wget nor curl is available..."
     exit 1