diff --git a/src/util/warning.ml b/src/util/warning.ml index a44af1295271c13fd3e4d253922e6efe6d341b0c..c2b2398647ad5df3f6557802849f1eeb1743ffb9 100644 --- a/src/util/warning.ml +++ b/src/util/warning.ml @@ -21,6 +21,8 @@ let set_hook = (:=) hook let emit ?loc p = let b = Buffer.create 100 in let fmt = formatter_of_buffer b in + pp_set_margin fmt 1000000000; + pp_open_box fmt 0; let handle fmt = - Format.pp_print_flush fmt (); !hook ?loc (Buffer.contents b) in + pp_print_flush fmt (); !hook ?loc (Buffer.contents b) in kfprintf handle fmt p