10 Nov
2008
10 Nov
'08
6:15 p.m.
On Wed, Oct 22, 2008 at 05:27:42PM +0200, Johannes Hofmann wrote:
On Wed, Oct 22, 2008 at 02:27:23PM +0000, corvid wrote:
I was changing the font in a few more places that can take arbitrary user text -- and then having to change it for neighbouring things so that the difference isn't too jarring -- and I reached the point where it seemed like it may be best just to change the font for everything.
I like it! We could also remove the places where the font has been set already.
Committed.
PS: In case someone needs it we could add a ui font option in dillorc and default to fw_fontname.
An ui_font_factor may be necessary. More in a next post... -- Cheers Jorge.-