aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index d7177044..418fbb4c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1675,7 +1675,7 @@ Near here means PT is either inside or just aside of a comment."
;; want xml like tags, and I want them removed before warning display.
;; I want the same for errors -> pgip
- proof-shell-eager-annotation-end "\377\\|done\\]\\|</infomsg>\\|\\*\\*\\*\\*\\*\\*\\|) >" ; done
+ proof-shell-eager-annotation-end coq-shell-eager-annotation-end ; done
proof-shell-annotated-prompt-regexp coq-shell-prompt-pattern
proof-shell-result-start "\372 Pbp result \373"
proof-shell-result-end "\372 End Pbp result \373"