Re: a new command that converts XML Texinfo to Texinfo

[Karl Berry]

    Should be fixed now (although I haven't tested).

I'm not seeing any difference ...

    I did quite a bit of testing along

Yeah, I got the impression that was happening from your commits.  Thanks
for all the info, that all makes sense and is good to know.

    I am not very eager to change all the files manually, 

Completely understandable.

    but I guess this could be automated.

It's not important to me if the change is made, I just wanted to make it
clear that I didn't object if you preferred the other way, to save the
source line ...

k