From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- lib/pp.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'lib/pp.mli') diff --git a/lib/pp.mli b/lib/pp.mli index 7917ba15..f292dedf 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -116,6 +116,7 @@ val msgnl : std_ppcmds -> unit val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit +val msg_warn : string -> unit (** Same specific display in emacs as warning, but without the "Warning:" **) val msg_debug : std_ppcmds -> unit -- cgit v1.2.3