Re: Options menu

[Luc Teirlinck]

David Kastrup wrote:

   > which we can not afford to re-open right now.

   Correct, but I don't see how it would be relevant.

Several ways.  For instance, in that discussion I believe I remember
that Kim proposed to remove the possibility of setting without saving
altogether.  I guess this will meet with disagreement from some
people, but if it does get adopted, it would make this entire
discussion completely moot.  All options set through Custom or the
Options menu would be saved, because we would have set == saved.

Sincerely,

Luc.