Re: strange looking HTML menus

[Karl Berry]

    Can someone please tell me why we have the final `:'?  

Just came out that way.  I agree it's not ideal.  I'll see what I can do.

    Additionally, the `--no-headers' is far too radical IMHO for HTML
    output; it also disables the very nice menu entries.  Is there a
    possibility to fine-tune this?

Anything's possible, but --no-headers omits the menus in Info output.  I
don't see any particular reason why they should be included in one case
and not the other.  If you want the menus, don't use --no-headers?  You
probably don't like that idea either, but the HTML output is never going
to please everyone ... I don't know.  There could always be another
option, but there's too many options already.

Stephen, since you just wrote about --no-headers, do you like or
dislike its exclusion of menus from html output?

Thanks,
k