added -nodb support

[helm.git] / helm / matita / matitamake.ml

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 _ =