From 1bbc2dd649df75e33f2cd7fb3e5ecb15f526a442 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Jun 2008 15:02:53 +0000 Subject: [PATCH] removed unused variable --- helm/software/matita/matitacLib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 9c836d9b8..7790f7568 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -259,7 +259,7 @@ 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 when not matita_debug -> + | Sys.Break when not matita_debug -> HLog.error "user break!"; pp_times fname false big_bang big_bang_u big_bang_s; clean_exit baseuri false -- 2.39.2