On Fri, Mar 26, 2021 at 04:18:50PM +0100, Ævar Arnfjörð Bjarmason wrote: > >> A small stand-alone series of doc infrastructure fixes. 5/6 fixes an > >> interesting bug that's been missed since doc-diff was introduced. > > > > I'm not sure what you mean about doc-diff here. Patch 5 (of 5?) doesn't > > seem related. Patch 4 is related only tangentially, in that you might > > have more stuff in your Documentation directory. > > That's how it's related, the lint script recursively looks for all *.txt > under Documentation/, before doc-diff we could safely assume this was > *.txt at that version of the repository, after doc-diff our recursively > search leads us to a different checkout at a different revision. > > I don't think it had any practical effect, just say'n. OK, thanks. I just wanted to make sure I wasn't missing something. -Peff