On 13 February 2016 at 03:55, Gavin Smith <[email protected]> wrote: > 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.
No-one's used this feature as far as I know, so I'm tempted to take it out until we can be more sure it's what we really want.
