On 2025-07-27 17:26, Stan Marsh wrote:
Just out of curiosity, I note that you (Paul) say that "pr" is "obsolete".This surprises me, since I still use it every day.
I'm not proposing that we remove pr, just that it's not high priority. As this is not a bug I'll be bold and close the bug report.But yes, pr is obsolete. Just like 'shred' is obsolete. Just like my car is obsolete. Doesn't mean we're gonna remove 'pr' or that I'll stop driving my car.