matitadep: we now handle the inline of an uri, we removed the -exclude option

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

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 129f2dabdce3545fc5efe7b185fc801b3fc791c7..5ca8ffc82a7f6f600303c41fe0d3c32afa6f6cbd 100644 (file)
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -170,10 +170,6 @@ let extra_cmdline_specs = ref []
 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 
 let parse_cmdline init_status =
-  let dump fname = 
-     let atexit = MatitacLib.dump fname in
-     at_exit atexit
-  in
   if not (already_configured [CmdLine] init_status) then begin
     wants [Registry] init_status;
     let includes = ref [] in
@@ -221,8 +217,6 @@ 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");
-        "-dump", Arg.String dump,
-          "<filename> Dump with expanded macros to <filename>";
         "-v", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
           "Verbose mode";