configure
changeset 29662 78c47f0002c3
parent 22722 03797b5d2ba3
child 47217 72e3ae9a25eb
--- a/configure	Mon Mar 23 11:44:40 2015 -0700
+++ b/configure	Thu Mar 26 16:17:30 2015 +0100
@@ -31,4 +31,5 @@
 
 # Delegate to wrapper, forcing wrapper to believe $0 is this script by using -c.
 # This trick is needed to get autoconf to co-operate properly.
-bash -c ". $this_script_dir/common/autoconf/configure" $this_script_dir/configure CHECKME $this_script_dir "$@"
+# The ${-:+-$-} construction passes on bash options.
+bash ${-:+-$-} -c ". $this_script_dir/common/autoconf/configure" $this_script_dir/configure CHECKME $this_script_dir "$@"