diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-11-07 22:00:54 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-11-07 22:00:54 +0000 |
| commit | fb37eba5deac15f470a858ede868dd22fa81309e (patch) | |
| tree | 888db789a8f550917084d5e9666c386e002a8a50 /BUGS | |
| parent | 0fdff8096d68fa6aa83c1f817f769e4b1f8a30af (diff) | |
Updated.
Diffstat (limited to 'BUGS')
| -rw-r--r-- | BUGS | 37 |
1 files changed, 33 insertions, 4 deletions
@@ -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. |