gui/gui-lib/mred
Matthew Flatt 5e70534b43 adjust workaround for GTK+3 before version 3.22
Adjust a workaround for versions before 3.22 when setting the font for
a control.

GTK+ version 3.22 starts paying attention to whether a font size for a
control is absolute (as opposed to being in points), so the workaround
that was put in place for earlier versions breaks.

In addition, some part of the drawing stack seems to round point sizes
to an integeral size after DPI conversion. Take that rounding into
account when setting the font size in `normal-control-font`.

Closes #1522
2016-12-19 07:21:28 -07:00
..
lang Remove extra directories. 2014-12-02 02:33:07 -05:00
private adjust workaround for GTK+3 before version 3.22 2016-12-19 07:21:28 -07:00
doc.txt Remove extra directories. 2014-12-02 02:33:07 -05:00
Draw_and_GUI_5_1.txt Remove extra directories. 2014-12-02 02:33:07 -05:00
edit-main.rkt Remove extra directories. 2014-12-02 02:33:07 -05:00
edit.rkt Remove extra directories. 2014-12-02 02:33:07 -05:00
HISTORY.txt Remove extra directories. 2014-12-02 02:33:07 -05:00
info.rkt cooperate with tethered-executable builds 2016-04-14 16:21:16 -06:00
installer.rkt cooperate with tethered-executable builds 2016-04-14 16:21:16 -06:00
main.rkt Remove extra directories. 2014-12-02 02:33:07 -05:00
MrEd_100_Framework.txt Remove extra directories. 2014-12-02 02:33:07 -05:00
MrEd_100.txt Remove extra directories. 2014-12-02 02:33:07 -05:00
mred-sig.rkt add any-control+alt-is-altgr 2016-03-17 16:39:40 -06:00
mred-unit.rkt Remove extra directories. 2014-12-02 02:33:07 -05:00
mred.1 Remove extra directories. 2014-12-02 02:33:07 -05:00
mred.rkt Remove extra directories. 2014-12-02 02:33:07 -05:00