summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2014-01-19 15:09:23 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2014-01-19 15:09:23 +0100
commitd2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch)
tree7b000ad50dcc45ff1c63768a983cded1e23a07ca /lib
parentdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff)
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'lib')
-rw-r--r--lib/pp.ml41
-rw-r--r--lib/pp.mli1
2 files changed, 2 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 569a028f..d3b402e3 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -341,6 +341,7 @@ let msgnl x = msgnl_with !std_ft x
let msgerr x = msg_with !err_ft x
let msgerrnl x = msgnl_with !err_ft x
let msg_warning x = msg_warning_with !err_ft x
+let msg_warn x = msg_warning (str x)
(* Same specific display in emacs as warning, but without the "Warning:" *)
let msg_debug x = msgnl (emacs_quote x)
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