Re: ugly menu in html

[Karl Berry]

      When I was using makeinfo (4.0), I found that the format of the menu
    in a html file was ugly. See the following test source:

Thanks for the report, I'll see what I can do.