when -debug do not catch the exception

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index f248545fba8c6d5caae409eb43fee604273185b2..a9172cee5a563b43406d37873a7eea76a72ee354 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -382,6 +382,7 @@ module F =
     ;;
 
     let build options fname =
     ;;
 
     let build options fname =

+      let matita_debug = Helm_registry.get_bool "matita.debug" in

       let compile opts fname =
         try
           GrafiteSync.push ();
       let compile opts fname =
         try
           GrafiteSync.push ();


@@ -395,7 +396,7 @@ module F =
             GrafiteParser.pop ();
             GrafiteSync.pop ();
             false
             GrafiteParser.pop ();
             GrafiteSync.pop ();
             false

-        | exn ->
+        | exn when not matita_debug ->

             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in