diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-21 15:11:23 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-23 14:37:20 +0200 |
commit | 59bb9b37c58e8b5f8d009d598e949aa995e6973e (patch) | |
tree | 5df6f98dfc385964a4e493b80de1a3190f9a67d6 /test-suite/bugs/opened/2572.v-disabled | |
parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) |
[toplevel] [emacs] Don't quote errors in emacs mode.
In 8.6 + emacs, errors were quoted sometimes with special
markers (e.g. `Print Module foo.` for a non-existing `foo`)
In 8.7 we uniformized error handling and now all errors are quoted,
however, this behavior confuses emacs as it seems that the quotes are
meant to be applied only to warnings.
We thus reflect the de-facto situation, removing quoting for errors
and updating the code so it is clear that the quoter is a warnings
quoter. We also update the warnings quoter to use a warning tag
instead of a non-printable char.
This fixes ProofGeneral for trunk users.
c.f. https://github.com/ProofGeneral/PG/issues/175
Diffstat (limited to 'test-suite/bugs/opened/2572.v-disabled')
0 files changed, 0 insertions, 0 deletions