diff options
Diffstat (limited to 'contrib/get-abc')
-rwxr-xr-x | contrib/get-abc | 29 |
1 files changed, 3 insertions, 26 deletions
diff --git a/contrib/get-abc b/contrib/get-abc index 7cf833e23..0a840fc84 100755 --- a/contrib/get-abc +++ b/contrib/get-abc @@ -1,37 +1,14 @@ #!/bin/bash # -set -e - -commit=53f39c11b58d - -cd "$(dirname "$0")/.." - -if ! [ -e src/parser/cvc/Cvc.g ]; then - echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 - echo "but apparently:" >&2 - echo >&2 - echo " $(pwd)" >&2 - echo >&2 - echo "is not a CVC4 source tree ?!" >&2 - exit 1 -fi - -function webget { - if which wget &>/dev/null; then - wget -c -O "$2" "$1" - elif which curl &>/dev/null; then - curl "$1" >"$2" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} +source "$(dirname "$0")/get-script-header.sh" if [ -e abc ]; then echo 'error: file or directory "abc" exists; please move it out of the way.' >&2 exit 1 fi +commit=53f39c11b58d + mkdir abc cd abc webget https://bitbucket.org/alanmi/abc/get/$commit.tar.gz abc-$commit.tar.gz |