]> matita.cs.unibo.it Git - helm.git/commitdiff
propagation of noinnertypes to matitac
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 16 Nov 2007 08:51:34 +0000 (08:51 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 16 Nov 2007 08:51:34 +0000 (08:51 +0000)
helm/software/matita/matitamakeLib.ml

index eed971f4514568a466e167165ef4781ed02c865d..2bf01f8979a32ad38caeb40cb80770c0d966c186 100644 (file)
@@ -215,7 +215,10 @@ let call_make ?matita_flags development target make =
     let system = 
       if Helm_registry.get_bool "matita.system" then " -system" else ""
     in
-    already_defined ^ bench ^ system
+    let noinnertypes = 
+      if Helm_registry.get_bool "matita.noinnertypes" then " -noinnertypes" else ""
+    in
+    already_defined ^ bench ^ system ^ noinnertypes
   in
   let csc = try ["SRC=" ^ Sys.getenv "SRC"] with Not_found -> [] in
   rebuild_makefile development;