changeset 28358 | 4be84366834a |
parent 24655 | 6940eba5402c |
child 28813 | 827e40c396a6 |
--- 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