problem with verbatim in html output

[Mike Benfield]

Hello,

I just discovered a bug in Texinfo 4.0. If there is a newer version and
this has been corrected please forgive me but I don't think that is the
case. Anyway the problem is that when makeinfo outputs HTML when it
comes to the @verbatim and @end verbatim commands, it makes <pre> tags
for the HTML but it doesn't do the closing tag correctly. It makes a tag
that looks like
/<pre>
instead of
</pre>

The problem is in the file makeinfo/insertion.c 
line 1061 reads
    add_word ("/<pre>");
but it should be
    add_word ("</pre>");

And there you have it. I would send a patch but it really doesn't seem
worth it. Anyway, just thought you'd like to know. Thanks for your
time and keep up the good work!

Mike Benfield