diff options
Diffstat (limited to 'contrib/get-script-header.sh')
-rw-r--r-- | contrib/get-script-header.sh | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh index de4a93587..4e2a133b3 100644 --- a/contrib/get-script-header.sh +++ b/contrib/get-script-header.sh @@ -1,6 +1,6 @@ -#!/bin/bash +#!/usr/bin/env bash # -set -e +set -e -o pipefail cd "$(dirname "$0")/.." @@ -15,12 +15,24 @@ 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 exit 1 fi } + +for cmd in python python2 python3; do + if [ -x "$(command -v $cmd)" ]; then + PYTHON="$cmd" + break + fi +done + +if [ -z "$PYTHON" ]; then + echo "Error: Couldn't find python, python2, or python3." >&2 + exit 1 +fi |