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

diff --git a/contrib/get-abc b/contrib/get-abc
index 7cf833e2348cedfcd354022bff9323480e74db16..0a840fc84b5a5362f79098635ec874127ba32a13 100755 (executable)
--- a/contrib/get-abc
+++ b/contrib/get-abc
@@ -1,37 +1,14 @@
 #!/bin/bash
 #
-set -e
-
-commit=53f39c11b58d
-
-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 abc ]; then
   echo 'error: file or directory "abc" exists; please move it out of the way.' >&2
   exit 1
 fi
 
+commit=53f39c11b58d
+
 mkdir abc
 cd abc
 webget https://bitbucket.org/alanmi/abc/get/$commit.tar.gz abc-$commit.tar.gz

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index 87d6ea450e2c10524d124b7461f69728765151b7..4ee23509aa3fedc7e3bcf1385cea31bf57569417 100755 (executable)
--- 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

diff --git a/contrib/get-cryptominisat4 b/contrib/get-cryptominisat4
index c96bbe03d046c2b935d3358ac68a3931d9e8cae5..c6f2a1ce8e4ecd88519dd61a75c69b301903f244 100755 (executable)
--- 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`

diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
index 5ca18c66d8fee3d2563ed81d9e80125ba15af48c..419fdba90963ae763e0b9bbcd2c377fe8027cf85 100755 (executable)
--- a/contrib/get-glpk-cut-log
+++ b/contrib/get-glpk-cut-log
@@ -1,32 +1,9 @@
 #!/bin/bash
 #
-set -e
+source "$(dirname "$0")/get-script-header.sh"
 
 commit=b420454e732f4b3d229c552ef7cd46fec75fe65c
 
-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
-}
-
 if [ -e glpk-cut-log ]; then
   echo 'error: file or directory "glpk-cut-log" exists; please move it out of the way.' >&2
   exit 1

diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 4950823879c50ed21bd95ded5abfefc3237eaad0..f4c79de2a304c9db6d71eba88c8c31608288b60a 100755 (executable)
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -1,23 +1,10 @@
 #!/bin/bash
 #
-set -e
+source "$(dirname "$0")/get-script-header.sh"
 
 lfscrepo="https://github.com/CVC4/LFSC.git"
 dirname="lfsc-checker"
 
-
-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 gitclone {
   if which git &> /dev/null
   then

diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh
new file mode 100644 (file)
index 0000000..285d97b
--- /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
+}