aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/pp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 4477d16567..bbd5c35207 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -371,7 +371,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 -> Flags.if_warn (msgnl_with !err_ft) (warnbody msg) (* bright yellow *)
+| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) () (* bright yellow *)
| Error -> msgnl_with !err_ft (errorbody msg) (* bright red *)
let logger = ref std_logger