diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-08-26 15:38:04 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-26 15:38:04 -0700 |
| commit | 9b9ecdf85954e937bd569cba018b6b09eee787a1 (patch) | |
| tree | 0d28bf7f9ba77e45ffba52cfe7913f8ee566bd79 /contrib/get-lfsc-checker | |
| parent | bf0c04f38a1dede1560bc880193889c6dd85ad67 (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/get-lfsc-checker')
| -rwxr-xr-x | contrib/get-lfsc-checker | 4 |
1 files changed, 2 insertions, 2 deletions
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 |