Configure option for flambda

1 files changed, 9 insertions, 0 deletions

diff --git a/configure b/configure
index d1d36094ac..b2c5f7d54e 100755
--- a/configure
+++ b/configure
@@ -51,6 +51,7 @@ no_naked_pointers=false
 native_compiler=true
 TOOLPREF=""
 with_cfi=true
+flambda=false
 
 # Try to turn internationalization off, can cause config.guess to malfunction!
 unset LANG
@@ -162,6 +163,8 @@ while : ; do
         with_cfi=false;;
     -no-native-compiler)
         native_compiler=false;;
+    -flambda)
+        flambda=true;;
     *) if echo "$1" | grep -q -e '^--\?[a-zA-Z0-9-]\+='; then
          err "configure expects arguments of the form '-prefix /foo/bar'," \
              "not '-prefix=/foo/bar' (note the '=')."
@@ -1788,6 +1791,7 @@ echo "HOST=$host" >> Makefile
 if [ "$ostype" = Cygwin ]; then
   echo "DIFF=diff -q --strip-trailing-cr" >>Makefile
 fi
+echo "FLAMBDA=$flambda" >> Makefile
 
 
 rm -f tst hasgot.c
@@ -1856,6 +1860,11 @@ else
   else
   inf "        profiling with gprof ..... not supported"
   fi
+  if test "$flambda" = "true"; then
+  inf "        using flambda middle-end . yes"
+  else
+  inf "        using flambda middle-end . no"
+  fi
 fi
 
 if test "$with_debugger" = "ocamldebugger"; then