X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitamakeLib.ml;h=2bf01f8979a32ad38caeb40cb80770c0d966c186;hb=f2e7cb9757a151382ed3a70d1a610e8f729a6597;hp=ccfdd9bab6f937754f98fe31ed7de9e420726010;hpb=5ce8c290c718dca7fd18d376b42108f8b947637b;p=helm.git

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index ccfdd9bab..2bf01f897 100644
--- a/matita/matitamakeLib.ml
+++ b/matita/matitamakeLib.ml
@@ -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;
@@ -355,7 +358,7 @@ let publish_development_bstract build clean devel =
     let orig_matita_flags = 
       try Sys.getenv "MATITA_FLAGS" with Not_found -> "" 
     in
-    "\"" ^ orig_matita_flags ^ "\"", "\"" ^ orig_matita_flags ^ " -system\"" 
+    orig_matita_flags, orig_matita_flags ^ " -system" 
   in
   HLog.message "cleaning the development before publishing";
   if clean ~matita_flags devel then