![]() because HINT doesn't works as expected, and the problem it seemed to solve at one time (slow resize in DrRacket) seems to have been fixed some other way. GDK_MOUSE_MOTION_MASK isn't needed, since GDK_POINTER_MOTION_MASK covers it. Merge to 5.1.2 |
||
---|---|---|
.. | ||
lang | ||
private | ||
doc.txt | ||
edit-main.rkt | ||
edit.rkt | ||
info.rkt | ||
installer.rkt | ||
main.rkt | ||
mred-sig.rkt | ||
mred-unit.rkt | ||
mred.rkt |