Re: menu-bar-options-save and menu-bar-options-menu

[Eli Zaretskii]

> From: "Drew Adams" <address@hidden>
> Date: Mon, 17 Jan 2005 21:17:57 -0800
> 
> I expect that modifying the Options menu will be one thing that customizing
> users will want to do - especially adding options that are toggles.

What options would you like to add?

At the time, the current list of options was carefully chosen so as to
include the most popular ones, but perhaps the list needs to be
revised (it's been almost 4 years since the last time, I think).

As for flexibility, I think the idea is that Customize is the flexible
machinery you are looking for.