diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/richpp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/richpp.mli b/ide/richpp.mli index 0fe4315b7a..ea4b189ba8 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -19,7 +19,7 @@ type 'annotation located = { (* XXX: The width parameter should be moved to a `formatter_property` record shared with Topfmt *) -(** [rich_pp width get_annotations ppcmds] returns the interpretation +(** [rich_pp width ppcmds] returns the interpretation of [ppcmds] as a semi-structured document that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired |