texinfo 5.00 -> 5.0 -> 4.13.90 html output

[Karl Berry]

Pat,

Looking at the top of HTML output just now, I was actually surprised to
see we are generating a doctype line now.  But ok, I can imagine it will
improve things nowadays.  In the past, it was a definite loser.

But anyway, what I really wanted to discuss was this line:
<!-- Created by Texinfo 5.00, http://www.gnu.org/software/texinfo/ -->

1) it should certainly not be 5.00 since we don't number the releases
like that.  It will be 5.0.  (I can imagine this came from CPAN-like
module numbering, which I know is done like that, which is more logical,
but ... too much history.)

2) but independent of that, this seems like one of the most important
places to use the real-life version number, namely 4.13.90.  Whether
it's actually derived from configure.ac or not isn't critical to me, but
I think it's important not to call it generated by 5.0 when it isn't.

Thanks,
k