ported to new getter interface

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

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index c16915e63c9cbeb11c97cf60a457104e746a2446..fbc393cfb3bed6472ae6de4874975b3786c632ff 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -108,11 +108,6 @@ let main ~mode =
   MatitaDb.create_owner_environment ();
 *)
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
-  at_exit
-    (fun () ->
-       Http_getter_logger.log "Sync map tree to disk...";
-       Http_getter.sync_dump_file ();
-       print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
   let fname = fname () in
   try
@@ -173,8 +168,8 @@ let main ~mode =
   | CicTextualParser2.Parse_error (floc,err) ->
      let (x, y) = CicAst.loc_of_floc floc in
      MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
-     Http_getter.sync_dump_file ();
      if mode = `COMPILER then
        exit 1
      else
        pp_ocaml_mode ()
+