The file is automatically generated. If you don't like how it is done bring it up with the texinfo maintainer. There is nothing special in what we do. Make sure you first get the latest and greatest version of texinfo and use it to create the HTML. -- â§ Ulrich Drepper â§ Red Hat, Inc. â§ 444 Castro St â§ Mountain View, CA â