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

1 files changed, 1 insertions, 1 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index c346943e15..4d2c866d10 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -341,7 +341,7 @@ let std_logger level msg = match level with
 | Debug _ -> msgnl (debugbody msg) (* cyan *)
 | Info -> msgnl (print_color "37" (hov 0 msg)) (* gray *)
 | Notice -> msgnl msg
-| Warning -> msgnl_with !err_ft (warnbody msg) (* bright yellow *)
+| Warning -> Flags.if_warn (msgnl_with !err_ft) (warnbody msg) (* bright yellow *)
 | Error -> msgnl_with !err_ft (errorbody msg) (* bright red *)
 
 let logger = ref std_logger