From 7321065b6dc1a2bba4dbb39d0570da3c62b30cfb Mon Sep 17 00:00:00 2001
From: mdenes
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
---
 lib/flags.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 727e2184b7..4ad929052d 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