From fb37eba5deac15f470a858ede868dd22fa81309e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 7 Nov 2002 22:00:54 +0000 Subject: Updated. --- BUGS | 37 +++++++++++++++++++++++++++++++++---- 1 file changed, 33 insertions(+), 4 deletions(-) (limited to 'BUGS') diff --git a/BUGS b/BUGS index 4b2c6fc4..345391c4 100644 --- a/BUGS +++ b/BUGS @@ -1,10 +1,39 @@ -*- outline -*- -* Bugs to be fixed before PG 3.4 is released. +* Bugs to be fixed before PG 3.5 is released. -The items below are known and will be fixed (I hope!) before 3.4 -is released. Please don't send email about them (unless you have -a patch...) +The items below are known and will be fixed before 3.5 is released. +Please don't send email about them (unless you can fix them). + + +** Problems with Red Hat 8.0 & (at least) Coq. + +Issue seems to be a problem with output handling arising in Coq +itself, perhaps caused by a change in the libraries(?) shipped with +RH8.0. Perhaps a 16-bit char problem (output is flushed before 16-bit +char is sent?). Example, run "coqtop -emacs" on MDK9.0 machine, +inside XEmacs (21.4.9) shell window, pressing return: + + [montague]da: coqtop -emacs + Welcome to Coq 7.3.1 (Oct 2002) + + Coq < ù + Coq < ù + Coq < ù + +Now do same thing on RH8 (21.4.8): + + [da@fraenkel generic]$ coqtop -emacs + Welcome to Coq 7.3.1 (Oct 2002) + + Coq < + ?< + ?< + +Same behaviour is seen in ordinary shell window, in fact. + + +================================================================= * Known Bugs and Workarounds for Proof General. -- cgit v1.2.3