From 08f4a234a669a2398be37c7fdab41ee9d3dcd6cd Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Mon, 11 Dec 2017 11:46:31 +0100
Subject: Fix #214.

If this works we should probably change the generic function as well.
---
 coq/coq.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index aff05d28..793c59a0 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -432,7 +432,8 @@ This is a subroutine of `proof-shell-filter'."
     (set-marker
      proof-shell-urgent-message-scanner
      (if end ;; couldn't find message start; move forward to avoid rescanning
-	 (max initstart
+         (max (or lastend 1) ;; goto after last end urgent msg
+              ;; or near the end of current output if that jumps farther.
 	      (- (point)
 		 (1+ proof-shell-eager-annotation-start-length)))
        ;; incomplete message; leave marker at start of message
-- 
cgit v1.2.3