aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index 4fea6b836..343588652 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -731,7 +731,7 @@ let save_library_to ?todo dir f otab =
let () = msg_warning (str ("Removed file "^f')) in
let () = close_out ch in
let () = Sys.remove f' in
- raise reraise
+ iraise reraise
let save_library_raw f lib univs proofs =
let (f',ch) = raw_extern_library (f^"o") in