aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre Courtieu2012-07-25 11:25:17 +0000
committerPierre Courtieu2012-07-25 11:25:17 +0000
commitd707721dba14a17d054ddb7c2e2d34e233d41e20 (patch)
treee360a9f3c30b40bcf6eaff6d911b58376c9d5cf4
parent5ade280786a6eb85c6b533cdf82cf9aafef1c8c5 (diff)
Cleaned up a obsolete regexp.
-rw-r--r--coq/coq.el2
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/coq.el b/coq/coq.el
index ef10b74d..95cdede0 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1084,7 +1084,7 @@ With flag Printing All if some prefix arg is given (C-u)."
;; 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 "\377\\|done\\]\\|</infomsg>\\|\\*\\*\\*\\*\\*\\*\\|) >" ; 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"