4593: Updating a StringOption option (via set_value()) does NOT update the GUI widget

svn: r17035

src/gui/plug/_guioptions.py

@@ -528,6 +528,11 @@ class GuiEnumeratedListOption(gtk.HBox):
         # signals don't fire)
 
         self.__option.set_value( value )
+        self.value_changed()    # Allow overriding so that another class
+                                # can add functionality
+        
+    def value_changed(self):
+        pass
 
     def __update_options(self):
         """