ported to new getter interface

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 3eb0fc6a15f985c897e07144b0949c41688805d7..251f7201767978af4fd88b6641356bb39fe6174e 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -148,12 +148,6 @@ let _ =
         (MatitaMathView.sequentViewer_instance ())#get_selected_terms);
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
-    addDebugItem "getter: update"
-      (fun _ ->
-         ignore (Thread.create (fun () ->
-           MatitaLog.message "Rebuilding getter maps in background ...";
-           Http_getter.update ();
-           MatitaLog.message "Getter maps successfully rebuilt.") ()));
     addDebugItem "getter: getalluris" (fun _ ->
       List.iter prerr_endline (Http_getter.getalluris ()));
     addDebugItem "dump script status" script#dump;
@@ -184,11 +178,7 @@ let _ =
   (** </DEBUGGING> *)
 
 let _ =
-  at_exit
-    (fun () ->
-       Http_getter_logger.log "Sync map tree to disk...";
-       Http_getter.sync_dump_file ();
-       print_endline "\nThanks for using Matita!\n");
+  at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
   (try
      gui#loadScript Sys.argv.(1);