projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
4365cdd
)
Follow redirects with cURL in contrib/get* scripts (#2471)
author
Andres Noetzli
<andres.noetzli@gmail.com>
Mon, 17 Sep 2018 19:16:07 +0000
(12:16 -0700)
committer
GitHub
<noreply@github.com>
Mon, 17 Sep 2018 19:16:07 +0000
(12:16 -0700)
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.
contrib/get-script-header.sh
patch
|
blob
|
history
diff --git
a/contrib/get-script-header.sh
b/contrib/get-script-header.sh
index 285d97b35d5b3fc38b995da5c48c641910f32275..de4a935875a008670ae9aa017199f99e797f8e66 100644
(file)
--- 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