Selection of font sizes is inconsistent
(First of all, great tool! I'm loving it so far.)
In the diff tool, the configure fonts and colors screen shows a different font size than the one I select in the font dialog that appears when clicking on "Change."
Example: (Consolas, Regular)
- If I pick size 9, the resulting font is Consolas, 9pt (ok)
- If I pick size 10, the resulting font is Consolas, 9.75pt (wrong)
- If I pick size 11, the resulting font is Consolas, 11.25pt (wrong)
5
votes

-
Violeta commented
In the font dialog, the number appears rounded, that is the reason. In the other view the number appears with decimal.