[Bug other/122638] makeinfo 4.7 chokes on several texinfo files

[sandra at gcc dot gnu.org via Gcc-bugs]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=122638

--- Comment #3 from sandra at gcc dot gnu.org ---
I also think it's reasonable to bump the minimum Texinfo version.  That said, I
think the attached patch fixes actual bugs in the .texi files and you can apply
it with my approval.