git-gui: Allow the user to manipulate the fonts from the options panel.
authorShawn O. Pearce <spearce@spearce.org>
Sun, 12 Nov 2006 10:27:00 +0000 (05:27 -0500)
committerShawn O. Pearce <spearce@spearce.org>
Sun, 12 Nov 2006 10:27:00 +0000 (05:27 -0500)
commit92148d8091d148e219b88e4d555a386ffa78f575
treee40ccb07118d43a7f50d8585dfda4bec521e7a5d
parent51f4d16b1d8e2e709f28a4e52b951236950cb1d5
git-gui: Allow the user to manipulate the fonts from the options panel.

This turned out to take a lot more time than I thought it would take;
but now users can edit the main UI font and the diff/fixed with font
by changing both the family name and/or the point size of the text.

We save the complete Tk font specification to the user's ~/.gitconfig
file upon saving options.  This is probably more verbose than it needs
to be as there are many useless options recorded (e.g. -overstrike 0)
that a user won't really want to use in this application.

Signed-off-by: Shawn O. Pearce <spearce@spearce.org>
git-gui