Closed akorobov closed 8 years ago
yep, fontsize is just an arbitrary number and I needed something that was factor 3:4 so it was either 9pt:12px or 12pt:16px
And since the font is ≈13px I changed it to 12px in https://github.com/larsenwork/monoid/commit/4bbcc3ee706d7d6d26fd30e0dc85fd23d7064ccf
It looks like font size in 0.60 was increased significantly. Here's comparison at size 11 of Menlo, Monoid 0.40 and 0.60:
Was this intentional?