On 12/31/18 1:14 PM, Per Bothner wrote:
If people are concerned about breaking things, I suggested adding --html4 and
--html5
as new output options. Only --html5 would create the new-style output.
The existing --html flag would be an alias to --html4. After a release or two
we could
change the default so --html is a default for --html5.
Simpler and easier to use would be either a customiation variable or an
environment variable:
MAKEINFO_HTML_OUTPUT=html5 makeinfo --html ...
--
--Per Bothner
[email protected] http://per.bothner.com/
