gui/gui-lib/mred
Matthew Flatt 5b7bf69a13 HiDPI support on Unix (Gtk2)
Support GUI scaling in much the same way as on Windows, where
the OS setting ("org.gnome.desktop.interface.scaling-factor"
times "...text-scaling-factor") determines the scale that is
used for both graphics and GUI sizing.

As I understand it, a complete solution requires porting to
Gtk3. With Gtk2, the graphical part of a widget doesn't scale.
Text and image labels should scale correctly, though.
2015-08-01 18:06:12 -06:00
..
lang Remove extra directories. 2014-12-02 02:33:07 -05:00
private HiDPI support on Unix (Gtk2) 2015-08-01 18:06:12 -06: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 Remove extra directories. 2014-12-02 02:33:07 -05:00
installer.rkt Remove extra directories. 2014-12-02 02:33:07 -05: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 Remove extra directories. 2014-12-02 02:33:07 -05: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