Re: [PATCH] gnome-terminal shortcut fonts menu

[Paul Warren <pdw ex-parrot com>]

On Tue, Jul 25, 2000 at 09:41:15PM -0400, Havoc Pennington wrote:
> 
> Paul Warren <pdw@ex-parrot.com> writes:
> > This patch adds the xterm-like feature of putting your favorite fonts on
> > the gnome-terminal menu.  It adds a "fonts" tab to the preferences
> > dialog allowing you to edit these fonts.
> > 
> > I've heard this feature requested on gnome-list a few times, and is also
> > wishlist item #3527.
> >
> 
> If you choose the font from the menu, is it just for a certain
> terminal or does it save it as the default config? (Personally the
> former sounds better to me.)

The former - to get the default font changed you need to Apply the font
in the preferences dialog.  Now that I think about it, this behaviour is
marginally yucky: if I change the font using the menu, and then go into
the preferences dialog, the font field will show the current font, but
the Apply button will be insensitive suggesting that the current font is
the font saved in the config, which is not the case.  

Not sure what the correct behaviour should be:
a) If current_font != config_font then Apply should be made sensitive as
soon as the prefs dialog is opened.
b) The field in the prefs dialog should show the config font rather than
the current font.
c) As it is.

I think (a).

> > I'd be grateful to hear any comments on this.  Is this correct place to
> > send patches?
> > 
> 
> Probably, but I'd also CC the gnome-terminal maintainers and stick it
> in the bug tracker, if you want to be sure it doesn't get forgotten.

OK - I'll implement (a) and fix the 1 letter typo in the patch and do
that.

cheers,

Paul