diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-11-29 14:44:04 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-11-29 14:44:04 +0000 |
| commit | cfdfac830bfc04a1b8c130396198c465b773ea27 (patch) | |
| tree | f88fc9e4f5b24313d394fd0166f35843480dcc49 /BUGS | |
| parent | 3d28f91919372c2ca54e097be8836f8530388594 (diff) | |
Note about duplicated messages.
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 8 |
1 files changed, 8 insertions, 0 deletions
@@ -83,6 +83,14 @@ using rsh instead, it is said to forward signals to the remote command. * In tty mode, the binding C-c C-RET has no effect. Workaround: manually bind C-c RET to 'proof-goto-point instead. +* You may occasionally see duplications of short (<10 chars) +messages from the proof assistant. This is caused by a too high +setting of the configuration variable +proof-shell-eager-annotation-start-length. +Add (setq proof-shell-eager-annotation-start-length 1) to your .emacs +if it bothers you badly. This fix will be made in the next +pre-release phase, it was too late to make it in time for testing for +release 3.0. LEGO Proof General Bugs |