From 2365a412571f633fc85633b134a45cf5a8777efa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 May 2007 15:53:33 +0000 Subject: [PATCH] fixed a when that was causing backtrace loss --- helm/software/components/library/librarySync.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 83f861b4e..e621a7a0c 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -444,6 +444,7 @@ let let add_obj refinement_toolkit uri obj = add_single_obj uri obj refinement_toolkit; let uris = ref [] in + let not_debug = not (Helm_registry.get_bool "matita.debug") in try begin match obj with @@ -474,9 +475,10 @@ let add_obj refinement_toolkit uri obj = end; UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris; !uris - with exn -> - List.iter remove_single_obj !uris; - raise exn + with + | exn when not_debug -> + List.iter remove_single_obj !uris; + raise exn let remove_obj uri = let uris = -- 2.39.2