Re: [PATCH 21.5] More texinfo 5.x changes