sphinx extension to output HTML help files