Use separate shell script for common get-* script parts. (#1567)

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