Browse Source

Refresh in any case; the user could have changed the refresh interval.

master
Julio Biason 14 years ago
parent
commit
de0e77fd47
  1. 3
      mitterlib/ui/ui_pygtk.py

3
mitterlib/ui/ui_pygtk.py

@ -751,8 +751,7 @@ class Interface(object):
value = int(value)
# if any of the options change, do another refresh
if (namespace != self.NAMESPACE and
self._options[namespace][option] != value):
if self._options[namespace][option] != value:
need_refresh = True
self._options[namespace][option] = value

Loading…
Cancel
Save