From 5ba84979df97996cd04f44e506742bb58ecf0465 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 16 Dec 2014 14:13:59 +0100
Subject: msg_info now puts infomsg tag in emacs mode.

Fixes the idtac "string" not appearing in proofgeneral because
printined *before* the goal.
---
 lib/pp.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index d4314a3366..9f65c0be0b 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -124,9 +124,9 @@ type logger = message_level -> std_ppcmds -> unit
 
 (** {6 output functions}
 
-[msg_info] and [msg_notice] do not put any decoration on output by
-default. If possible don't mix them with goal output (prefer
-msg_warning) so that dispatching of outputs is easier. Once all
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
 interfaces use the xml-like protocol this constraint can be
 relaxed. *)
 (* Should we advertise these functions more? Should they be the ONLY
-- 
cgit v1.2.3