From 7321065b6dc1a2bba4dbb39d0570da3c62b30cfb Mon Sep 17 00:00:00 2001
From: mdenes <mdenes@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 24 Feb 2013 11:56:32 +0000
Subject: New -no-native-compiler flag for configure, globally disabling the
 native compiler (implemented on Matthieu's request).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16240 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 config/coq_config.mli |  1 +
 configure             | 13 ++++++++++++-
 lib/flags.ml          |  2 +-
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/config/coq_config.mli b/config/coq_config.mli
index f2861f12a..f16ffbe51 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -69,3 +69,4 @@ val wwwrefman : string
 val wwwstdlib : string
 val localwwwrefman : string
 
+val no_native_compiler : bool
diff --git a/configure b/configure
index c799254ad..d68a4d87e 100755
--- a/configure
+++ b/configure
@@ -89,7 +89,9 @@ usage () {
     echo "-typerex"
     printf "\tCompiles Coq using typerex wrapper\n"
     echo "-makecmd <command>"
-    printf "\tName of GNU Make command.\n"
+    printf "\tName of GNU Make command\n"
+    echo "-no-native-compiler"
+    printf "\tDisables compilation to native code for conversion and normalization\n"
 }
 
 
@@ -142,6 +144,7 @@ with_doc_spec=no
 force_caml_version=no
 force_caml_version_spec=no
 usecamlp5=yes
+no_native_compiler=false
 
 # Parse command-line arguments
 
@@ -249,6 +252,7 @@ while : ; do
     -profile|--profile) coq_profile_flag=-p;;
     -annotate|--annotate) coq_annotate_flag=-dtypes;;
     -typerex|--typerex) coq_typerex_wrapper=$default_typerex_wrapper;;
+    -no-native-compiler|--no-native-compiler) no_native_compiler=true;;
     -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) 
           force_caml_version_spec=yes
 	  force_caml_version=yes;;
@@ -901,6 +905,11 @@ echo "  Web browser                       : $BROWSER"
 echo "  Coq web site                      : $WWWCOQ"
 echo ""
 
+if test "$no_native_compiler" = "true"; then
+echo "  Native compiler for conversion and normalization disabled"
+echo ""
+fi
+
 if test "$local" = "true"; then
 echo "  Local build, no installation..."
 echo ""
@@ -1051,6 +1060,8 @@ let wwwcoq = "$WWWCOQ"
 let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
 let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
 let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
+let no_native_compiler = $no_native_compiler
+
 
 END_OF_COQ_CONFIG
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 727e2184b..4ad929052 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -168,7 +168,7 @@ let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
 
 (* Disabling native code compilation for conversion and normalization *)
-let no_native_compiler = ref false
+let no_native_compiler = ref Coq_config.no_native_compiler
 
 (* Print the mod uid associated to a vo file by the native compiler *)
 let print_mod_uid = ref false
-- 
cgit v1.2.3