22 Oct
2008
22 Oct
'08
4:32 p.m.
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.