diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-03 19:38:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-03 21:29:02 +0100 |
| commit | ec4ce9efc02d0f908a7f54ca47520703673e74c4 (patch) | |
| tree | 598541a7ddf2442a5c6b455326d4c344b6da56ef /lib/pp.ml | |
| parent | 3ad26e3de5780b84b2723d44d52094bab6b23786 (diff) | |
Tracking memory misallocation by trying to improve sharing.
Diffstat (limited to 'lib/pp.ml')
| -rw-r--r-- | lib/pp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |