From dd4088ade7539c42adb15f58edcbf7fcf638731c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Sep 2016 09:40:39 +0200
Subject: CoqIDE: push to message win feedback Message(Debug,Info,Notice)

---
 ide/coqOps.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 52f935bf66..1563c7ffb4 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -481,6 +481,8 @@ object(self)
           add_flag sentence (`WARNING (loc, msg));
           self#attach_tooltip sentence loc msg;
           self#position_warning_tag_at_sentence sentence loc
+      | Message((Info|Notice|Debug as lvl), _, msg), _ ->
+          messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
           else to_process <- to_process + n
-- 
cgit v1.2.3