On Tuesday, August 20, 2024 at 8:56:15 AM UTC-7 julian...@fsfe.org wrote:
implies that "disputed" label is only for a PR that has positive review from a reviewer but another still objects it. I think adding "disputed" label prematurely is not appropriate. Then who can remove the "disputed" label in this case? That's not how I interpret the policy we have. I think the idea is to first use the "needs whatever" labels and when no agreement can be reached, then "disputed" can be set. Julian, that contradicts the entirety of the past practice that you carried out on behalf of the committee when you removed lots of "disputed" labels earlier this year. -- 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 on the web visit https://groups.google.com/d/msgid/sage-devel/dd5ae63b-4235-4dea-8b5c-b13b7574e8ean%40googlegroups.com.
