X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitac.ml;h=b3767c5397cf3477ad62c607f9df011a0e8d48bb;hb=dab3163daed8034aca17b9ed18d5200e4b9f046a;hp=ef0ab5a99ccf6fcbb170294ad0b0343e9add02a4;hpb=e6708c10ad615233628900902101216cc2f5baf5;p=helm.git 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)