diff options
Diffstat (limited to 'contrib/get-script-header.sh')
-rw-r--r-- | contrib/get-script-header.sh | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh new file mode 100644 index 000000000..285d97b35 --- /dev/null +++ b/contrib/get-script-header.sh @@ -0,0 +1,26 @@ +#!/bin/bash +# +set -e + +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 +} |