summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2019-08-26 15:38:04 -0700
committerGitHub <noreply@github.com>2019-08-26 15:38:04 -0700
commit9b9ecdf85954e937bd569cba018b6b09eee787a1 (patch)
tree0d28bf7f9ba77e45ffba52cfe7913f8ee566bd79 /contrib
parentbf0c04f38a1dede1560bc880193889c6dd85ad67 (diff)
Make contrib/get-* more robust. (#3198)
We use the command which to determine if a command is available on the system. However, which is not installed on all platforms by default (e.g. CentOS). command is a shell builtin that can be used for the same purpose.
Diffstat (limited to 'contrib')
-rwxr-xr-xcontrib/get-abc2
-rwxr-xr-xcontrib/get-antlr-3.42
-rwxr-xr-xcontrib/get-cryptominisat2
-rwxr-xr-xcontrib/get-drat2er2
-rwxr-xr-xcontrib/get-glpk-cut-log2
-rwxr-xr-xcontrib/get-gmp2
-rwxr-xr-xcontrib/get-lfsc-checker4
-rw-r--r--contrib/get-script-header.sh4
-rwxr-xr-xcontrib/get-symfpu2
-rwxr-xr-xcontrib/get-win-dependencies10
10 files changed, 17 insertions, 15 deletions
diff --git a/contrib/get-abc b/contrib/get-abc
index fa90f240f..5d3f32fb5 100755
--- a/contrib/get-abc
+++ b/contrib/get-abc
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index a3dfb410d..ecc92d998 100755
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -34,7 +34,7 @@ cd $ANTLR_HOME_DIR || exit 1
webget https://www.antlr3.org/download/antlr-3.4-complete.jar share/java/antlr-3.4-complete.jar
webget https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz src/libantlr3c-3.4.tar.gz
tee bin/antlr3 <<EOF
-#!/bin/bash
+#!/usr/bin/env bash
export CLASSPATH=`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH
exec java org.antlr.Tool "\$@"
EOF
diff --git a/contrib/get-cryptominisat b/contrib/get-cryptominisat
index 6b3a7029a..379d75df1 100755
--- a/contrib/get-cryptominisat
+++ b/contrib/get-cryptominisat
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
diff --git a/contrib/get-drat2er b/contrib/get-drat2er
index e465ab3d4..52c663ab3 100755
--- a/contrib/get-drat2er
+++ b/contrib/get-drat2er
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
if [ -e drat2er ]; then
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
index dcd5aac00..85ea643a9 100755
--- a/contrib/get-glpk-cut-log
+++ b/contrib/get-glpk-cut-log
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
diff --git a/contrib/get-gmp b/contrib/get-gmp
index 02602e456..aec125185 100755
--- a/contrib/get-gmp
+++ b/contrib/get-gmp
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
# This script should only be used if your distribution does not ship with the
# GMP configuration you need. For example, contrib/get-win-dependencies
diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 2fc191707..953d05d18 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
@@ -6,7 +6,7 @@ lfscrepo="https://github.com/CVC4/LFSC.git"
dirname="lfsc-checker"
function gitclone {
- if which git &> /dev/null
+ if [ -x "$(command -v git)" ]
then
git clone "$1" "$2"
else
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh
index e5b708042..4e2a133b3 100644
--- a/contrib/get-script-header.sh
+++ b/contrib/get-script-header.sh
@@ -15,9 +15,9 @@ if ! [ -e src/parser/cvc/Cvc.g ]; then
fi
function webget {
- if which wget &>/dev/null; then
+ if [ -x "$(command -v wget)" ]; then
wget -c -O "$2" "$1"
- elif which curl &>/dev/null; then
+ elif [ -x "$(command -v curl)" ]; then
curl -L "$1" >"$2"
else
echo "Can't figure out how to download from web. Please install wget or curl." >&2
diff --git a/contrib/get-symfpu b/contrib/get-symfpu
index a31d27e06..b17c00299 100755
--- a/contrib/get-symfpu
+++ b/contrib/get-symfpu
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
source "$(dirname "$0")/get-script-header.sh"
diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index f3fbd6cf7..1138e3071 100755
--- a/contrib/get-win-dependencies
+++ b/contrib/get-win-dependencies
@@ -1,10 +1,12 @@
-#!/bin/bash
+#!/usr/bin/env bash
#
# win32-build script
# Morgan Deters <mdeters@cs.nyu.edu>
# Tue, 15 Jan 2013 11:11:24 -0500
#
+set -e -o pipefail
+
export WINDOWS_BUILD=yes
export MAKE_CFLAGS=
export MAKE_CXXFLAGS=
@@ -50,10 +52,10 @@ function reporterror {
}
function webget {
- if which curl &>/dev/null; then
- curl -L "$1" >"$2"
- elif which wget &>/dev/null; then
+ if [ -x "$(command -v wget)" ]; then
wget -c -O "$2" "$1"
+ elif [ -x "$(command -v curl)" ]; then
+ curl -L "$1" >"$2"
else
echo "Can't figure out how to download from web. Please install wget or curl." >&2
exit 1
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback