Ensure that the texinfo manual can be converted to HTML.

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.