diff options
Diffstat (limited to 'vernac/topfmt.ml')
| -rw-r--r-- | vernac/topfmt.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index c25dd55fb..2f01cfb54 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -108,7 +108,7 @@ end type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit -let msgnl_with ?pre_hdr fmt strm = +let msgnl_with fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () |