author | ihse |
Thu, 15 Jan 2015 15:43:28 +0100 (2015-01-15) | |
changeset 28358 | 4be84366834a |
parent 28357 | 75a20253de17 |
child 28359 | 3a02fb1e9144 |
--- a/common/autoconf/configure Thu Jan 15 15:40:56 2015 +0100 +++ b/common/autoconf/configure Thu Jan 15 15:43:28 2015 +0100 @@ -36,6 +36,13 @@ shift fi +if test "x$BASH" = x; then + echo "Error: This script must be run using bash." 1>&2 + exit 1 +fi +# Force autoconf to use bash +export CONFIG_SHELL=$BASH + conf_script_dir="$TOPDIR/common/autoconf" if [ "$CUSTOM_CONFIG_DIR" = "" ]; then