From d63320ceb1c56710f5e953742dd5d6cf43aacbdf Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 8 May 2013 19:55:23 +0000
Subject: Uniformizing the [if_warn] flag used for warning printing and put it
 into the standard logger instead.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/loadpath.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/loadpath.ml')

diff --git a/library/loadpath.ml b/library/loadpath.ml
index 873703aff..60799a8a7 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -74,7 +74,7 @@ let add_load_path phys_path isroot coq_path =
       begin
         (* Assume the user is concerned by library naming *)
         if not (DirPath.equal dir Nameops.default_root_prefix) then
-          Flags.if_warn msg_warning
+          msg_warning
             (str phys_path ++ strbrk " was previously bound to " ++
               pr_dirpath dir ++ strbrk "; it is remapped to " ++
               pr_dirpath coq_path);
-- 
cgit v1.2.3