Re: makeinfo options

[Jonathan S. Shapiro]

> There's no reason to make readers gratuitiously
> barf on documents that happen to be generated with a new version of
> makeinfo.

I think you misunderstood me. I don't propose to change the output of
makeinfo, so I don't think the readers would be impacted. Rather, I propose
to identify the version of the makeinfo *input*.

This does not introduce backward incompatibility. Input that is compatible
with older versions of makeinfo simply omits the @infoversion tag.