git-gui: Corrected font used for options menu items.
Signed-off-by: Shawn O. Pearce <spearce@spearce.org>
This commit is contained in:
parent
1daf1d0c81
commit
058803f400
1
git-gui
1
git-gui
@ -1677,6 +1677,7 @@ menu .mbar.push
|
|||||||
menu .mbar.options
|
menu .mbar.options
|
||||||
.mbar.options add checkbutton \
|
.mbar.options add checkbutton \
|
||||||
-label {Trust File Modification Timestamps} \
|
-label {Trust File Modification Timestamps} \
|
||||||
|
-font $font_ui \
|
||||||
-offvalue false \
|
-offvalue false \
|
||||||
-onvalue true \
|
-onvalue true \
|
||||||
-variable cfg_trust_mtime
|
-variable cfg_trust_mtime
|
||||||
|
Loading…
Reference in New Issue
Block a user