summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/library.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index c857fc86..8620c0a5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -656,7 +656,7 @@ let save_library_to dir f =
System.marshal_out ch table;
close_out ch
with reraise ->
- warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise
+ msg_warn ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise
(************************************************************************)
(*s Display the memory use of a library. *)