aboutsummaryrefslogtreecommitdiffhomepage
path: root/BUGS
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-03-20 17:39:20 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-03-20 17:39:20 +0000
commitc1dfa794d88a256f17b42adae220df694c5e4ea3 (patch)
treebed89904bbd785ff642e10f7ac10a1794361d1a1 /BUGS
parent67735f434627c4bfbc0bedd9a64bb824581efde7 (diff)
strange buffer selection bug reported by Markus
Diffstat (limited to 'BUGS')
-rw-r--r--BUGS7
1 files changed, 5 insertions, 2 deletions
diff --git a/BUGS b/BUGS
index 86ba12e6..ec72973a 100644
--- a/BUGS
+++ b/BUGS
@@ -77,9 +77,12 @@ simplifier, when tracing rewriting.
Workaround: manually bind C-c RET to 'proof-goto-point instead.
+** Active minibuffer can cause strange buffer selection behaviour.
-
-
+Try this: start PG/isar, step into a proof, activate a mini buffer (by
+visit-file etc.), now update goals output by clicking the toolbar. PG
+will attempt to put the output into the minibuffer portion of the
+frame! To get back to a sane state, use C-]
* Problems with particular Emacs versions