Re: address@hidden: documentation bug: customization type `option']

[Richard Stallman]

    Nevertheless, it might be nice to document these, since the widget
    manual is the place where programmers go to look for information
    about widgets.  Certainly I did...  :)

If you would like these to be better documented,
I recommend adding information to their doc strings.
It is not worth writing text in the manual for internal facilities.
Writing good manual text is hard work, and I don't want to do it
when it's not needed.