]> https://gitweb.dealii.org/ - dealii.git/commitdiff
Only use progress bar in wget if available 6653/head
authorDaniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Wed, 23 May 2018 11:35:21 +0000 (13:35 +0200)
committerDaniel Arndt <daniel.arndt@iwr.uni-heidelberg.de>
Wed, 23 May 2018 11:57:53 +0000 (13:57 +0200)
contrib/utilities/download_clang_format

index a73956184793ad5c7e1b9997f3931d3f4960e879..d02752266c71705e2c5b9284191da51522f17d91 100755 (executable)
@@ -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

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.