added -nodb support

diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml
index 8bd5900f5b10d99bcfa105a3aef0179d731f2d4b..b967fee19e530d39431fe06cc83ae44e7058cd90 100644 (file)
--- a/helm/matita/matitamake.ml
+++ b/helm/matita/matitamake.ml
@@ -122,6 +122,12 @@ let build_dev args =
   | false -> exit 1
 ;; 
 
+let nodb_doc = "
+\tParameters:
+\tDescription: avoid using external database connection."
+
+let nodb _ = Helm_registry.set_bool "db.nodb" true
+
 let target args = 
   if List.length args < 1 then !usage ();
   let dev = dev_for_dir (Unix.getcwd ()) in
@@ -137,6 +143,7 @@ let params = [
   "-list", list_dev, list_dev_doc;
   "-destroy", destroy_dev, destroy_dev_doc;
   "-build", build_dev, build_dev_doc;
+  "-nodb", nodb, nodb_doc;
   "-h", (fun _ -> !usage()), "print this help screen";
   "-help", (fun _ -> !usage()), "print this help screen";
 ]
@@ -156,13 +163,14 @@ usage := fun () ->
   exit 1
 ;;
  
-let parse args = 
+let rec parse args = 
   match args with
   | [] -> target ["all"]
   | s::tl ->
       try
         let _,f,_ = List.find (fun (n,_,_) -> n = s) params in
-        f tl
+        f tl;
+        parse tl
       with Not_found -> if s.[0] = '-' then !usage () else target args
   
 let _ = 

diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml
index 16f2c67c6fd41b9006a9bdbad4aec64be3b85da6..998dcd70edf225f595509a23ff822d715f63fb98 100644 (file)
--- a/helm/matita/matitamakeLib.ml
+++ b/helm/matita/matitamakeLib.ml
@@ -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