From 9d51b4473dd2b28eae6dd9800ca54d7247d6af1b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 7 Oct 2005 08:52:19 +0000 Subject: [PATCH] added -nodb support --- helm/matita/matitamake.ml | 12 ++++++++++-- helm/matita/matitamakeLib.ml | 7 ++++++- 2 files changed, 16 insertions(+), 3 deletions(-) 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 -- 2.39.2