X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=8f164b73aca1f5d0f71196630e7415962bfa8e74;hb=ebe70c001a623e0440f21cd16dc88f585edcf0ea;hp=16f2c67c6fd41b9006a9bdbad4aec64be3b85da6;hpb=b2f2e47efe1e01df81cb7659c30eeb76f1f830da;p=helm.git

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 16f2c67c6..8f164b73a 100644
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -25,10 +25,10 @@
 
 let logger = fun mark -> 
   match mark with 
-  | `Error -> MatitaLog.error
-  | `Warning -> MatitaLog.warn
-  | `Debug -> MatitaLog.debug
-  | `Message -> MatitaLog.message
+  | `Error -> HLog.error
+  | `Warning -> HLog.warn
+  | `Debug -> HLog.debug
+  | `Message -> HLog.message
 ;;
 
 type development = 
@@ -171,8 +171,13 @@ let make chdir args =
 let call_make development target make =
   rebuild_makefile development;
   let makefile = makefile_for_development development in
+  let nodb =
+    Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb"
+  in
+  let flags = if nodb then ["NODB=true"] else [] in
   make development.root 
-    ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target]
+    (["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target]
+    @ flags)
       
 let build_development ?(target="all") development =
   call_make development target make
@@ -186,21 +191,20 @@ let vt100 s =
   let rex_d = Pcre.regexp "^Debug" in
   let rex_noendline = Pcre.regexp "\\n" in
   let s = Pcre.replace ~rex:rex_noendline s in
-  let len = String.length s in
   let tokens = Pcre.split ~rex s in
-  let logger = ref MatitaLog.message in
+  let logger = ref HLog.message in
   let rec aux = 
     function
     | [] -> ()
     | s::tl ->
         (if Pcre.pmatch ~rex:rex_i s then
-          logger := MatitaLog.message
+          logger := HLog.message
         else if Pcre.pmatch ~rex:rex_w s then
-          logger := MatitaLog.warn
+          logger := HLog.warn
         else if Pcre.pmatch ~rex:rex_e s then
-          logger := MatitaLog.error
+          logger := HLog.error
         else if Pcre.pmatch ~rex:rex_d s then
-          logger := MatitaLog.debug
+          logger := HLog.debug
         else 
           !logger s);
         aux tl