X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;fp=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=5ca8ffc82a7f6f600303c41fe0d3c32afa6f6cbd;hb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;hp=129f2dabdce3545fc5efe7b185fc801b3fc791c7;hpb=298868e07163c21863d542136733d24bfbec2482;p=helm.git

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 129f2dabd..5ca8ffc82 100644
--- 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";