Hello Patrice and Gavin,
thanks for your answers.
>> Why `<pre>`? I consider this surprising since the item description
>> of a menu entry (i.e., the third part of an entry) is not output
>> with `<pre>`.
>
> The idea was that the users may have wanted to have the end lines
> and spaces to be significant, like in Info output. I agree that it
> is somewhat inconsistent to have menu comments in preformatted and
> not menu entries with descriptions. I think that there was
> previously the possibility to have menu entries also in preformatted
> like menu comments, with the SIMPLE_MENU option, but it is gone, it
> was too much of a pain to keep up to date.
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).
Werner
