One possible approach to adding info.js support to makeinfo is using
--set-customization-variable. It has the advantage that people can request
this feature without breaking it using older versions of makeinfo.
--set-customization-variable js-info-dir=DIRECTORY
This adds to each output file:
<link rel="stylesheet" type="text/css" href="DIRECTORY/info.css"/>
<script src="DIRECTORY/modernizr.js" type="text/javascript"></script>
<script src="DIRECTORY/info.js" type="text/javascript"></script>
and copies the 3 files to DIRECTORY (under the output directory).
--
--Per Bothner
[email protected] http://per.bothner.com/
