aboutsummaryrefslogtreecommitdiffhomepage
path: root/BUGS
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2008-07-24 09:51:53 +0000
commit76d6b0b2b1f039549d308a0d2c478a6b05869af9 (patch)
tree78cc7e13bf290a17e7006a6d4616a8a08e36ce8f /BUGS
parent8f8e9388b582ad6d3ee6e1eea842a8d443d4ce89 (diff)
Merge changes from Version4Branch.
Diffstat (limited to 'BUGS')
-rw-r--r--BUGS7
1 files changed, 0 insertions, 7 deletions
diff --git a/BUGS b/BUGS
index b9f3c4d6..3535dce5 100644
--- a/BUGS
+++ b/BUGS
@@ -84,13 +84,6 @@ The code is not fully protected from Emacs interrupts.
Workaround: Don't type C-g while script management is processing.
If you do, use proof-restart-scripting to be sure of synchronizing.
-** Outline-mode does not work in processed proof script files
-
-Because of read-only restrictions of the protected region.
-This is an inherent problem with outline because it works by
-modifying the buffer.
-Workaround: none.
-
** When proof-rsh-command is set to "ssh host", C-c C-c broken
The whole process may be killed instead of interrupted. This isn't a