>> OK, so please document this. Looking at section `Writing a menu`
>> in the Texinfo info file (of current git) I don't see anything
>> about HTML output of `@menu` blocks and how it is formatted (and
>> the description of `FORMAT_MENU` doesn't mention this either).
>
> In general, we do not describe how output is formatted in the manual
> except in rare cases. It seems to me that the formatting of menu
> comments is not something we want to document, we do not want to set
> expectations on a way to format or another. For example, we could
> switch to formatting menu entries with <pre>.
Well, you don't have to go into details, but I as a user want to know
whether menu descriptions are output pre-formatted in HTML mode also.
You eventually have to find a solution that looks good both in Info
and in HTML mode, which is an unusual combination in Texinfo.
Werner
