aboutsummaryrefslogtreecommitdiffhomepage
path: root/BUGS
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-11-25 14:10:31 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-11-25 14:10:31 +0000
commit3588aca7b6d5edebcde7a32e24d43531c35d85aa (patch)
treef1f2ba14f1f6457594ce97636cdbb683095d9201 /BUGS
parent73a59aba07146650d43fe3f7151114afa7d0c4be (diff)
Updated
Diffstat (limited to 'BUGS')
-rw-r--r--BUGS16
1 files changed, 11 insertions, 5 deletions
diff --git a/BUGS b/BUGS
index be0f5e1b..0b2c57b4 100644
--- a/BUGS
+++ b/BUGS
@@ -1,10 +1,15 @@
-Known Bugs and Workarounds.
-===========================
+Known Bugs and Workarounds for Proof General.
+=============================================
$Id$
-* Toolbar: retract button can give "BUG" error message "called from
-wrong buffer" when the process is inactive.
+Contact: proofgen@dcs.ed.ac.uk
+See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS
+
+-----------------
+
+Generic problems
+================
* Ordinary undo in script buffer can edit the "uneditable region"
in XEmacs. This doesn't happen in FSFmacs. Test case:
@@ -41,7 +46,8 @@ get a patch from Sun, or use Linux.
* XEmacs sessions perhaps grow excessively in terms of memory
allocation. Maybe some of the spans aren't removed properly.
Setting a limit on the size of the process buffer doesn't seem to
-help. (1998/10/06: Is this bug still present? Test examples?)
+help. (1998/10/06: Is this bug still present? Please tell us if
+you think so.)
*`proof-find-next-terminator' (bound to C-c C-e) doesn't work
properly. Workaround: use other means to navigate in a proof scipt