diff -r 68def6418e33 -r 5e8e88da4416 configure
--- a/configure	Wed Apr 08 14:32:34 2015 -0700
+++ b/configure	Wed Jul 05 20:27:01 2017 +0200
@@ -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 "$@"