# HG changeset patch
# User ihse
# Date 1421333008 -3600
# Node ID 4be84366834a5c96e3bd0c34c19a3582cbd96871
# Parent  75a20253de17adc8b127ce697e28fe831f5540b3
8069057: Make sure configure is run by bash
Reviewed-by: erikj

diff -r 75a20253de17 -r 4be84366834a common/autoconf/configure
--- 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