Merge (with minor modifications) some fixes for safety wrt font names and rounding background darkness values

This commit is contained in:
Chris Jones 2010-04-02 15:04:44 +01:00
commit 6a2d75c33c
1 changed files with 5 additions and 4 deletions

View File

@ -244,8 +244,11 @@ class PrefsEditor:
self.on_system_font_checkbutton_toggled(widget) self.on_system_font_checkbutton_toggled(widget)
# Font selector # Font selector
widget = guiget('font_selector') widget = guiget('font_selector')
if self.config['use_system_font'] == True: if self.config['use_system_font'] == True:
widget.set_font_name(self.config.get_system_font()) fontname = self.config.get_system_font()
if fontname is not None:
widget.set_font_name(fontname)
else: else:
widget.set_font_name(self.config['font']) widget.set_font_name(self.config['font'])
# Allow bold text # Allow bold text
@ -547,9 +550,7 @@ class PrefsEditor:
def on_darken_background_scale_change_value(self, widget, scroll, value): def on_darken_background_scale_change_value(self, widget, scroll, value):
"""Background darkness setting changed""" """Background darkness setting changed"""
# FIXME: 'value' is a float with way too much precision. Round it off self.config['background_darkness'] = round(value, 2)
# to 1 significant digit, e.g. 0.9 not 0.89989888413241345
self.config['background_darkness'] = value
self.config.save() self.config.save()
def on_background_image_filechooser_file_set(self, widget): def on_background_image_filechooser_file_set(self, widget):