On 9 February 2016 at 02:31, Per Bothner <[email protected]> wrote: >>> and then add the following in the <head>: >>> >>> <script type="text/javascript" src="info.js"></script> >> >> >> How do people add this in the <head>? By typing it in with a text >> editor? With a browser plugin that adds the line automatically? > > > Of course not. > >> That's the kind of specific point that needs to be taken care of. > > > The obvious simply approach is to add --javascript-include and/or > --javascript-ref command-line options to makeinfo, by analogy > with --css-include and --css-ref.
I hadn't thought of that possibility. These options seem like a good idea to me, and should be easy to implement.
