diff options
Diffstat (limited to 'lib/pp.mli')
| -rw-r--r-- | lib/pp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pp.mli 10803 2008-04-16 09:30:05Z cek $ i*) +(*i $Id$ i*) (*i*) open Pp_control @@ -85,7 +85,7 @@ val warning_with : Format.formatter -> string -> unit val warn_with : Format.formatter -> std_ppcmds -> unit val pp_flush_with : Format.formatter -> unit -> unit -val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit +val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit (*s Pretty-printing functions \emph{with flush}. *) |