The top node was made conditional with the @iftex command, since it should not
appear in PostScript and PDF output. However, it is still necessary for
texi2html, so we have to use @ifnottex instead.
Texi2html also complains about the use of @cindex in the copyright statement,
so we remove that.