From abea1aa1f1e152be1809145c962fa6588728d6f7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 14:11:02 +0000 Subject: [PATCH] The getter maps are now dumped also if matitac exits abruptly. --- helm/matita/matitac.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index ef0ab5a99..b3767c539 100644 --- 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) -- 2.39.2