The getter maps are now dumped also if matitac exits abruptly.

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

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index ef0ab5a99ccf6fcbb170294ad0b0343e9add02a4..b3767c5397cf3477ad62c607f9df011a0e8d48bb 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -83,7 +83,14 @@ let run_script fname =
       raise exn
         
 let _ = 
-  List.iter (fun fname -> 
+  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;
+  try
+   List.iter (fun fname -> 
     let time = Unix.time () in
     MatitaLog.message (sprintf "execution of %s started:" fname);
     run_script fname;
@@ -100,7 +107,5 @@ let _ =
     in
     MatitaLog.message 
       (sprintf "execution of %s completed in %s." fname (hou^min^sec))) scripts;
-  Http_getter.sync_dump_file ();
-  exit(0)
-  
-
+    exit(0)
+  with Sys.Break -> exit (-1)