aboutsummaryrefslogtreecommitdiff
path: root/library/lib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/lib.ml')
-rw-r--r--library/lib.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 46a2833f57..ea81207871 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -192,5 +192,7 @@ let unfreeze stk =
let init () =
lib_stk := [];
add_frozen_state ();
- path_prefix := []
+ path_prefix := [];
+ init_summaries()
+