On Saturday, January 25, 2025 at 5:35:47 AM UTC+9 Nils Bruin wrote: On Friday, 24 January 2025 at 11:28:42 UTC-8 axio...@yahoo.de wrote:
To do this, it is very helpful that unfinished tickets are *not* closed, because this gives me the "interesting" tickets with a single click: I hide all the closed ones. Usually only a few remain, and the older among those tell me the story I want to listen to. That's a relevant data point: indeed, "stale" PRs are not "closed" PRs (which would include integrated PRs and truly discarded ones). I agree with this view. A stale PR (with unresponsive author) should not be closed, because it is related with an open issue. Having unresponsive author is rather the state of the review process. A reviewer may tag it with the existing label "pending" or with "s: needs info" until the author returns, to warn off other reviewers. The "stale" PRs need to be differentiated from them so that they can show up in searches. So perhaps "closing" them isn't the right thing to do. Searches also show closed PRs in the "closed" tab. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/sage-devel/364f8d99-08a8-4ce7-afe4-10056bb58fb8n%40googlegroups.com.
