makeinfo options

[Jonathan S. Shapiro]

The --html option to makeinfo should not imply --no-split, as these two behaviors are independent, and HTML splitting may be implemented in the future. Until HTML splitting is implemented, makeinfo should complain if --no-split has not been specified. This change should be made now to avoid unexpected consequences in future builds as makeinfo evolves.   Similarly, the --no-headers should not have implications for output redirection. The two are completely orthogonal.   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.     shap