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`