When running the makeinfo-command to create the HTML documentation in
docs/htmldocs the resulting index.html file is a collision between the
top node and the documentation of the 'index' command. Check it out.
Clicking the "Top" link on all pages (except) on index.html leads to
index.html. But there the link leads to a non-existing file. Also
index.html mixes the top "menu" structure and the description of the