Re: Bug, probably related to Custom Themes.

[Luc Teirlinck]

Chong Yidong wrote:

   Maybe the "Save Options" menu bar entry should unconditionally save
   all these options.  The current behavior, which is to check the
   saved-value of the option against its default-value, doesn't seem to
   be necessary.

Then you would get the opposite problem: hardcoding a bunch of
settings to their default values, thereby overriding future themes,
without the user having asked for that.

Sincerely,

Luc.