aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2017-12-11 11:46:31 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2017-12-11 11:46:31 +0100
commit08f4a234a669a2398be37c7fdab41ee9d3dcd6cd (patch)
tree56eaee19916cef175535fc806b2df8d80fc13d14
parent2eab72c33751768c8a6cde36b978ea4a36b91843 (diff)
Fix #214.
If this works we should probably change the generic function as well.
-rw-r--r--coq/coq.el3
1 files changed, 2 insertions, 1 deletions
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