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.

1 files changed, 1 insertions, 1 deletions

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"