On 23 August 2024 09:05:55 BST, Kwankyu Lee <ekwan...@gmail.com> wrote:
>On Wednesday, August 21, 2024 at 12:56:15 AM UTC+9 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. If we had to wait for a "positive review", then
>there would be a race condition of sorts: You'd have to be fast so the
>release manager does not pick the PR up while the positive review label is
>set.
>
>
>OK. That concern is reasonable. Then at least there should be explicit
>issues (expressed in comments) on which the author and the negative
>reviewer disagrees before "disputed" label is added.
This doesn't work well with blocked GitHub users allowed for some reason in our
project - one cannot directly comment on, or review, PRs whose authors block
other users. Such users can still change labels,
to indicate disagreement.
Dima
>
>
>
>
--
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/5873F5C0-3AD0-42C2-A7F4-A7AA268FB2DD%40gmail.com.
