Procedural: we corrected two errors about the handling of mutcase (the "cases"

[helm.git] / helm / software / matita / matitaInit.ml

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index f75cbcf483472fd9d6d091315b108ec69f46bdbe..aee55d60d0292f73d7261d0e3a1d3fb294f57567 100644 (file)
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -192,6 +192,7 @@ let parse_cmdline init_status =
           (HExtlib.normalize_path (absolutize path)^" "^uri)
       | _ -> raise (Failure "bad baseuri, use -b 'path::uri'")
     in
+    let no_default_includes = ref false in
     let arg_spec =
       let std_arg_spec = [
         "-b", Arg.String set_baseuri, "<path::uri> forces the baseuri of path";
@@ -217,10 +218,12 @@ let parse_cmdline init_status =
               Helm_registry.set_bool "matita.system" true),
             ("Act on the system library instead of the user one"
              ^ "\n    WARNING: not for the casual user");
-        "-v", 
+        "-no-default-includes", Arg.Set no_default_includes,
+          "Do not include the default searched paths for the include command"; 
+       "-v", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
           "Verbose mode";
-        "--version", Arg.Unit print_version, "Prints version";
+        "--version", Arg.Unit print_version, "Prints version"
       ] in
       let debug_arg_spec =
         if BuildTimeConf.debug then
@@ -240,6 +243,7 @@ let parse_cmdline init_status =
       Helm_registry.set_list Helm_registry.of_string ~key ~value:l
     in
     Arg.parse arg_spec (add_l args) (usage ());
+    let default_includes = if !no_default_includes then [] else default_includes in
     let includes = 
       List.map (fun x -> HExtlib.normalize_path (absolutize x)) 
        ((List.rev !includes) @ default_includes)