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
gui	Remove extra directories.	2014-12-02 02:33:07 -05:00
gui-doc	document non-empty str requirement for text% find-string methods	2016-12-15 16:00:05 -06:00
gui-lib	adjust workaround for GTK+3 before version 3.22	2016-12-19 07:21:28 -07:00
gui-test	adjust replace-all so that it accounts for the possibility that the text didn't go away	2016-12-14 15:21:36 -06:00
tex-table	some more updates to follow TeX better for \var vs non-\var greek letters	2016-03-10 21:54:30 -06:00
.gitignore	Add standard .gitignore file.	2014-12-06 17:46:34 -05:00