Re: find.texi Texinfo fixes

[James Youngman]

Sorry, I had applied your patch of the previous day, but missed this
one.  It's now applied.