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 135343092d..8b3f6ff244 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -103,7 +103,6 @@ val pp : std_ppcmds -> unit val ppnl : std_ppcmds -> unit val pperr : std_ppcmds -> unit val pperrnl : std_ppcmds -> unit -val message : string -> unit (** = pPNL *) val pp_flush : unit -> unit val flush_all: unit -> unit @@ -122,6 +121,7 @@ val msg : std_ppcmds -> unit val msgnl : std_ppcmds -> unit val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit +val message : string -> unit (** = pPNL *) (** {6 Location management. } *) |