From cfdfac830bfc04a1b8c130396198c465b773ea27 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 29 Nov 1999 14:44:04 +0000 Subject: Note about duplicated messages. --- BUGS | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'BUGS') diff --git a/BUGS b/BUGS index 0fb4e142..afb4152a 100644 --- a/BUGS +++ b/BUGS @@ -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 -- cgit v1.2.3