From: Daniel Arndt 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