R devel - Oct 2010 - Documentation of option 'help.ports' not in help("options")

FYI,

the option 'help.ports' is not document under help("options").
Should
it?  It is documented under help("startDynamicHelp",
package="tools").

This is for for R v2.13.0dev and Rv2.12.0.

/Henrik

>>>>> Henrik Bengtsson <hb at stat.berkeley.edu>
>>>>>     on Wed, 27 Oct 2010 12:54:15 -0700 writes:
    > FYI,
    > the option 'help.ports' is not document under
help("options").  Should
    > it?  
yes, for completeness' sake; I've added it besides the other
help.<foobar> options.

    > It is documented under help("startDynamicHelp",
package="tools").

    > This is for for R v2.13.0dev and Rv2.12.0.

Thank you, Henrik, for the notice.
Martin