On Tue, Aug 04, 2020 at 07:11:10PM -0700, Per Bothner wrote: > 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).
Good idea. I think this is the way forward. Then we can work on the various issues that you found.
