Does anything actually use this file? It doesn't appear to be used for generating the HTML manuals.
It looks like we might use it for latex, man and texinfo output from sphinx judging by docs/conf.py, but I don't think we actually use sphinx to generate such output, so I think this is all dead code. Am I mistaken? --js
