On Tue, Dec 15, 2020 at 2:48 PM Alejandro Colomar (man-pages) <[email protected]> wrote: > > 1) Remove that paragraph, as if that behavior had never existed.
If it's been 15 years since that paragraph was relevant, I think just
removing it is the right thing to do.
Linus

