diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 17:08:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-15 17:08:31 +0000 |
| commit | 5c58f544019e666aafc574a4f543a3baa87d6ad3 (patch) | |
| tree | 3cf6cb28cb07a2f6e9e8396ac37261eed6a75d7b | |
| parent | fb0868cf2fde231d280e7410771dde1dd10b1759 (diff) | |
Updated.
| -rw-r--r-- | etc/README | 10 | ||||
| -rw-r--r-- | etc/bug-notes.txt | 16 |
2 files changed, 6 insertions, 20 deletions
@@ -14,10 +14,12 @@ ProofGeneral.desktop Menu file for some Linux versions. announce Announcement -lego Files for testing LEGO Proof General -isa Isabelle Proof General -isar Isar PG -demoisa Isabelle Demo PG +lego Files for testing: LEGO Proof General +isa Isabelle Proof General +isar Isar PG +demoisa Isabelle Demo PG +coq Coq +<otherprover> .. others, similarly bug-notes.txt Test cases for Emacs or PG bugs diff --git a/etc/bug-notes.txt b/etc/bug-notes.txt index c4aaf21d..e00a23e7 100644 --- a/etc/bug-notes.txt +++ b/etc/bug-notes.txt @@ -6,22 +6,6 @@ Test cases for PG and/or Emacs bugs. ---------------- -* Coq, and others bug: synchronization not gained until second line. - -Test in Coq buffer: - - Print foo. - -Should give error, but PG ignores it and colours command blue. -Similar errors for some other provers. - -[ Now fixed in 3.2pre ] - - - - ----------------- - * XEmacs bug: buffer-syntactic-context-depth returns weird values Seems to depend on previous history. Test in Coq buffer: |