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-antlr-3.4 | |
parent | 341728ed95dcff20fd75bb7aef4e0b7773f63e07 (diff) |
Use separate shell script for common get-* script parts. (#1567)
Diffstat (limited to 'contrib/get-antlr-3.4')
-rwxr-xr-x | contrib/get-antlr-3.4 | 25 |
1 files changed, 1 insertions, 24 deletions
diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index 87d6ea450..4ee23509a 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -1,34 +1,11 @@ #!/bin/bash # -set -e - -cd "$(dirname "$0")/.." +source "$(dirname "$0")/get-script-header.sh" if [ -z "${BUILD_TYPE}" ]; then BUILD_TYPE="--disable-shared --enable-static" fi -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 curl &>/dev/null; then - curl "$1" >"$2" - elif which wget &>/dev/null; then - wget -c -O "$2" "$1" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} - if [ -z "${MACHINE_TYPE}" ]; then if ! [ -e config/config.guess ]; then # Attempt to download once |