I am running makeinfo 3.12h, and yes, I will upgrade before posting anything
else. However, in the interest of complete understanding:
> > Similarly, the --no-headers should not have implications for output
> > redirection. The two are completely orthogonal.
>
> Sorry, I don't understand what do you mean here. How does
> "--no-headers" imply something about redirection?
Under makeinfo 3.12h, using makeinfo --help, the --no-headers option is
documented to suppress node headers and force output to standard out in the
absence of --output.
> > Finally, some mechanism should be introduced to allow control over
> > content in the HTML header. In particular, some means is needed to
> > introduce style sheets.
>
> Can't this be done with @html?
Possibly. Where can @html be used to ensure that the html output ends up
between the <head>..</head> tags rather than in the body? I have not been
able to figure this out.
