diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-04-24 11:28:59 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-04-24 11:28:59 +0200 |
| commit | 758e679ebcfce22099ba4b360b7c0ed7bee2a736 (patch) | |
| tree | 4025f1637cd6953f5223bd134feaf0c6786330d7 /coq/coq.el | |
| parent | 03ff7c4c6bfd666c3aa394eb981ccd7d762acf8c (diff) | |
Preparing new warning tags (no more special chars).
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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" |