+1 On Mon, 4 Mar 2024 at 20:21, G. M.-S. <lists....@gmail.com> wrote: > > > +1 > > Guillermo > > On Mon, 4 Mar 2024 at 09:43, David Roe <roed.m...@gmail.com> wrote: >> >> The following proposal has been made several times the last few weeks: in PR >> #37428, in this thread and then in this thread. It is orthogonal to the >> ongoing vote in this thread. With no further discussion, I'm calling a vote. >> >> Background >> >> Starting in Sage 10.2, PRs with the Blocker label have been merged into all >> other PRs before running CI; see the changelog and this post for more >> details. This has led to disagreements about whether this label should be >> applied. >> >> Proposal >> We use "CI Fix" rather than Blocker to determine whether an open PR should >> be merged before running CI. Blocker will retain its previous meaning of a >> PR that should be merged before the next release is finished. The process >> below describes how to resolve disagreements about whether the "CI Fix" >> label should be applied. >> a. Only PRs with positive review should be marked with the "CI Fix" label. >> This should be done if both author and reviewer agree that it is >> appropriate, and a rationale should be given in a comment on the ticket. >> b. If a PR becomes disputed (as described in this proposal), the "CI Fix" >> status can be voted on separately upon request; otherwise it should be >> applied if and only if positive review is applied. >> >> Voting will be open until Wednesday, March 13. >> David > > > -- > 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/CANnG189Rx%3DfXHDCQvDiTS0f_qHwRG9LbfiKKqph6DXuF%3Dd1zcw%40mail.gmail.com.
-- 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/CAGEwAAm6wy1c4mDnvfwT5Ow%2BCEYvheqKDyzOpTfjJZUd_Ur%3DNQ%40mail.gmail.com.
