aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/summary.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/summary.ml')
-rw-r--r--library/summary.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/library/summary.ml b/library/summary.ml
index af4deb40f..dcc6cce90 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,7 +107,11 @@ let unfreeze_summary datas =
List.iter
(fun (id, data) ->
let summary = Hashtbl.find summaries id in
- summary.unfreeze_function data)
+ try summary.unfreeze_function data
+ with e ->
+ let e = Errors.push e in
+ prerr_endline ("Exception unfreezing " ^ id);
+ raise e)
datas
(** All-in-one reference declaration + registration *)