From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 7 Oct 2005 08:52:19 +0000 (+0000)
Subject: added -nodb support
X-Git-Tag: V_0_7_2_3~230
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d51b4473dd2b28eae6dd9800ca54d7247d6af1b;p=helm.git

added -nodb support
---

diff --git a/helm/matita/matitamake.ml b/helm/matita/matitamake.ml
index 8bd5900f5..b967fee19 100644
--- 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 16f2c67c6..998dcd70e 100644
--- 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