changeset 1295:da879ffb91cc

8069057: Make sure configure is run by bash Reviewed-by: erikj
author ihse
date Thu, 15 Jan 2015 15:43:28 +0100
parents e881be6b7af7
children f1dc16345985
files common/autoconf/configure
diffstat 1 files changed, 7 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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