[karl@gnu.org: [texinfo-pretest] texinfo 4.7.91 pretest available]

[Karl Berry]

    talking about changing only 2 file names, which shouldn't be a
    problem.  Or is it?

Yes, unfortunately, it is.  Those files come from gnulib, and they
should be changed at the source, I can't easily change them just for
texinfo (and don't want to).  Especially since there are other
workarounds, ugly as they are.

Perhaps one of you could write bug-gnulib at gnu.org about the problem?

Thanks,
karl