common/autoconf/configure
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