diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/clib.mllib | 5 | ||||
| -rw-r--r-- | lib/pp.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib index a9b596b99e..022a14ac36 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -1,3 +1,5 @@ +Coq_config + Int Option Store @@ -5,8 +7,8 @@ Exninfo Backtrace IArray Pp_control +Flags Pp -Coq_config Deque Hashset Hashcons @@ -18,6 +20,5 @@ Util Loc Serialize Xml_utils -Flags CUnix Envars @@ -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 |