22 Oct
2008
22 Oct
'08
5:37 p.m.
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. Cheers, Johannes PS: In case someone needs it we could add a ui font option in dillorc and default to fw_fontname.