diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-02-06 19:46:04 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-06 19:46:04 -0800 |
commit | a9c5063145f3870393dc2dd75d0722ead1c5efd7 (patch) | |
tree | 2a345327e0dcc6acd7aec4355a04ee504141816e /contrib/get-cryptominisat4 | |
parent | 341728ed95dcff20fd75bb7aef4e0b7773f63e07 (diff) |
Use separate shell script for common get-* script parts. (#1567)
Diffstat (limited to 'contrib/get-cryptominisat4')
-rwxr-xr-x | contrib/get-cryptominisat4 | 29 |
1 files changed, 3 insertions, 26 deletions
diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4 index c96bbe03d..c6f2a1ce8 100755 --- a/contrib/get-cryptominisat4 +++ b/contrib/get-cryptominisat4 @@ -1,37 +1,14 @@ #!/bin/bash # -set -e - -version="4.2.0" - -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 cryptominisat4 ]; then echo 'error: file or directory "cryptominisat4" exists; please move it out of the way.' >&2 exit 1 fi +version="4.2.0" + mkdir cryptominisat4 cd cryptominisat4 CRYPTOMINISAT_PATH=`pwd` |