(defun manual-misc-html (name root html-node-dir html-mono-dir)
;; Hack to deal with the cases where .texi creates a different .info.
(defun manual-misc-html (name root html-node-dir html-mono-dir)
;; Hack to deal with the cases where .texi creates a different .info.