Make contrib/get-* more robust. (#3198)
authorMathias Preiner <mathias.preiner@gmail.com>
Mon, 26 Aug 2019 22:38:04 +0000 (15:38 -0700)
committerGitHub <noreply@github.com>
Mon, 26 Aug 2019 22:38:04 +0000 (15:38 -0700)
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.

contrib/get-abc
contrib/get-antlr-3.4
contrib/get-cryptominisat
contrib/get-drat2er
contrib/get-glpk-cut-log
contrib/get-gmp
contrib/get-lfsc-checker
contrib/get-script-header.sh
contrib/get-symfpu
contrib/get-win-dependencies

index fa90f240f42cabc08fd384f8572f253b904fde7d..5d3f32fb5a8ddf097f6d85766c80e10b697bb8a8 100755 (executable)
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
index a3dfb410d163b78b340a4a723df9b206b725606d..ecc92d9981f123baf5607dcde4e9cdd78ac07d52 100755 (executable)
@@ -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
index 6b3a7029a062817a15ef5346dc3e71245ca0dad6..379d75df1d299c63aaa61b647e632496e5a756b1 100755 (executable)
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
index e465ab3d43f3a16d07ee674f4a1f45660f3624d5..52c663ab35d8ed94b887c43b2cea8b2463223927 100755 (executable)
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 if [ -e drat2er ]; then
index dcd5aac002d36d5370195ae3d7043a96ea0444ce..85ea643a92fb4f087c5a1ef70743cced40730ff0 100755 (executable)
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
index 02602e456dd0958cd9798ea8cbee3b0062200de7..aec125185396d0b2ac1d0d2be240adf02f81aa2f 100755 (executable)
@@ -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
index 2fc191707aed0caaefdd4ab730d36f010dc315a0..953d05d18000b3e166af9e52e53c989a066cc4c6 100755 (executable)
@@ -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
index e5b7080420e9279fb024a7015b3815cf2d83d87f..4e2a133b3a2e88c9b72e46011f60693342e0b4c1 100644 (file)
@@ -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
index a31d27e06258a54ef021ccd8187fe112511eabcf..b17c0029917cbe1dc86a72ffdb5c1a330d274460 100755 (executable)
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
index f3fbd6cf7848efd856a42914689590069b9097cb..1138e3071556793dfe5172365a9a7fb11958021c 100755 (executable)
@@ -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