However, please consider whether it would be better to set this option on the command line rather than inside the Texinfo file itself as it may not be the best place for controlling details of the output.
An idea is to add support to makeinfo so that it reads a makeinfo.conf file (or equivalent) in the current working directory, which would contain all the options a user might want to pass to makeinfo.
