On Sun, Aug 25, 2024 at 11:33:45AM +0100, Gavin Smith wrote: > > I think it is most likely a mistake.
Another possibility would be that the manual name got renamed and the old name is used here. But even if it was the case, the new name should be there too, and there should be a comment explaining the situation. -- Pat
