From c0731d1fa3ae894da2473541a759d48e9b76613a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Jun 2008 12:02:10 +0000 Subject: [PATCH] when -debug do not catch --- helm/software/matita/matitacLib.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 8808aea22..9c836d9b8 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -259,13 +259,11 @@ let compile options fname = LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status; pp_times fname false big_bang big_bang_u big_bang_s; clean_exit baseuri false - | Sys.Break as exn -> - if matita_debug then raise exn; + | Sys.Break as exn when not matita_debug -> HLog.error "user break!"; pp_times fname false big_bang big_bang_u big_bang_s; clean_exit baseuri false - | exn -> - if matita_debug then raise exn; + | exn when not matita_debug -> HLog.error ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); pp_times fname false big_bang big_bang_u big_bang_s; -- 2.39.2