diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp.mli b/lib/pp.mli index 56e66225c..ca62f82d6 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -89,7 +89,7 @@ val msg_with : Format.formatter -> std_ppcmds -> unit val msgnl_with : Format.formatter -> std_ppcmds -> unit -(** {6 Sect } *) +(** {6 ... } *) (** The following functions are instances of the previous ones on [std_ft] and [err_ft]. *) |