From 5c58f544019e666aafc574a4f543a3baa87d6ad3 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 15 Apr 2004 17:08:31 +0000 Subject: Updated. --- etc/README | 10 ++++++---- etc/bug-notes.txt | 16 ---------------- 2 files changed, 6 insertions(+), 20 deletions(-) diff --git a/etc/README b/etc/README index 62c7c417..6b622f9b 100644 --- a/etc/README +++ b/etc/README @@ -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 + .. 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 @@ -4,22 +4,6 @@ $Id$ 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 -- cgit v1.2.3