From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 19 Jan 2014 15:09:23 +0100
Subject: Imported Upstream version 8.4pl3dfsg

---
 library/library.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

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. *)
-- 
cgit v1.2.3