>>>>> "John" == John Levon <[EMAIL PROTECTED]> writes:
John> On Wed, Jan 09, 2002 at 11:08:32PM +0200, Dekel Tsur wrote: >> Recently, the font in the menus became bold. Is it intentional ? John> actually a bug got fixed (by Angus) John> check your preferences and change the menu settings to medium John> instead of bold. Actually I think the bug has not been fixed in the right way: when I did the new menu thing a long time ago, I decided that having menus in bold was stupid, so that I switched to using normal font. So we had two fonts: - one for normal popup text and menus - one for bold text in popups. The problem is that the second one is still named menu_font. So the right fix obviously is just to rename this menu_font variable to alt_font or whatever. But it seems I got lazy and forgot to do/propose it. Would it be a problem to rename the variable? Of course this mens people will get errors when reading their preference file until they apply preferences, but we could also have compatibility code. Or we could keep the name of the variable but change its help text and GUI. Sorry for the inconvenience. JMarc
