diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2001-03-20 17:39:20 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2001-03-20 17:39:20 +0000 |
commit | c1dfa794d88a256f17b42adae220df694c5e4ea3 (patch) | |
tree | bed89904bbd785ff642e10f7ac10a1794361d1a1 /BUGS | |
parent | 67735f434627c4bfbc0bedd9a64bb824581efde7 (diff) |
strange buffer selection bug reported by Markus
Diffstat (limited to 'BUGS')
-rw-r--r-- | BUGS | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -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 |