Log Message:
Don't patch both the texinfo file and the generated info file.  This
avoids problems with timestamps and make's dependency graph calculations.