diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-17 12:16:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-17 12:16:07 -0700 |
| commit | fc07d6af4156fde8af048ca5db8ff1f43de48ebc (patch) | |
| tree | 3a6a102e9fd9558562a787ca3fc1537b07177df9 | |
| parent | 4365cdd8c582e2d1a3d406f5395d4950270f8c83 (diff) | |
Follow redirects with cURL in contrib/get* scripts (#2471)
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
| -rw-r--r-- | contrib/get-script-header.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh index 285d97b35..de4a93587 100644 --- a/contrib/get-script-header.sh +++ b/contrib/get-script-header.sh @@ -18,7 +18,7 @@ function webget { if which wget &>/dev/null; then wget -c -O "$2" "$1" elif which curl &>/dev/null; then - curl "$1" >"$2" + curl -L "$1" >"$2" else echo "Can't figure out how to download from web. Please install wget or curl." >&2 exit 1 |