From bfde711dd3ecd1065c8cbc6d321c583b1ac5d6c5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 3 Oct 2008 11:06:40 +0000
Subject: [PATCH] when -debug do not catch the exception

---
 helm/software/matita/matitacLib.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index f248545fb..a9172cee5 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -382,6 +382,7 @@ module F =
     ;;
 
     let build options fname =
+      let matita_debug = Helm_registry.get_bool "matita.debug" in
       let compile opts fname =
         try
           GrafiteSync.push ();
@@ -395,7 +396,7 @@ module F =
             GrafiteParser.pop ();
             GrafiteSync.pop ();
             false
-        | exn ->
+        | exn when not matita_debug ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in
-- 
2.39.2