Fixes for short output duplication problem: set proof-shell-eager-annotation-start-length.

1 files changed, 1 insertions, 0 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 76abab6c..fbd85399 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -502,6 +502,7 @@
         proof-shell-field-char ?\374 ; not done
         proof-shell-goal-char ?\375 ; done
 	proof-shell-eager-annotation-start "\376" ; done
+	proof-shell-eager-annotation-start-length 1
 	proof-shell-eager-annotation-end "\377" ; done
         proof-shell-annotated-prompt-regexp
 	(concat proof-shell-prompt-pattern