Re: texinfo 7.0.3; the main menu is missing in HTML output.

On Tue, Aug 08, 2023 at 01:17:06PM +0000, Alan Mackenzie wrote:
> Hello, Gavin.
> 
> On Mon, Aug 07, 2023 at 23:25:42 +0100, Gavin Smith wrote:
> > On Mon, Aug 07, 2023 at 09:16:36PM +0000, Alan Mackenzie wrote:
> 
> [ .... ]
> 
> > To get the menus output in HTML, use the FORMAT_MENU variable.  It
> > would look like "texi2any -c FORMAT_MENU=menu my-manual.texi".
> 
> Thanks for such a rapid and helpful reply!  That works!
> 
> I don't think there's a link to this option from the manual section on
> @menu, though.
> 
> [ .... ]

I've reworded it and added a cross-reference:

--- a/doc/texinfo.texi
+++ b/doc/texinfo.texi
@@ -2831,9 +2831,10 @@ @node Menus
 @findex menu
 
 @dfn{Menus} contain pointers to subordinate nodes.  In Info output,
-you use menus to go to such nodes.  Menus can be used in HTML output
-but are not used in the default case.  Menus have no role in printed
-manuals or other output formats.
+you use menus to go to such nodes.  @command{texi2any} can output menus in
+HTML output, but does not do so by default
+(@pxref{Other Customization Variables}, under @code{FORMAT_MENU}).
+Menus have no role in printed manuals or other output formats.
 
 Menus are automatically generated by @command{texi2any} when outputting
 Info for nodes followed by a sectioning command, without an explicit