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. > > It might be desirable to "plug in" user-selectable JavaScript > user-interface libraries on the fly depending on the user preference, > but the simple makeinfo-time --javascript-ref option will do to start with.
Added in revision 7007. If it looks good, I'll add the option to the documentation.
