Dear all, as discussed at some length in https://groups.google.com/d/msg/sage-devel/tQhromqp9hQ/KDCvCnKEd1kJ , the release manager expects us not to push to a ticket after it has been set to positive_review.
The reason is that merging a ticket is not an atomic step, but takes several hours, so the old commit might be merged without anyone noticing. This occurred in 6 or 7 tickets over the last year. Several alternative policies have been proposed, as far as I can see, none of them reached consensus. So in order to avoid losing any more commits, I propose ticket #18228 to mitigate the possible damage: document the semantics of "positive_review" as it is used in the current workflow. Clearly, this means that - even if we find a typo in a docstring in a ticket which is set to positive_review, we have to open a new ticket instead of simply changing the existing one - even if we think that a particular ticket should not be merged even if somebody else gave a positive review, we are not expected to set it back to needs_work, as it might be merged anyway. This post is meant to raise awareness of this issue as the subject of the previous thread might not have caught attention. Regards, Clemens Heuberger -- 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 post to this group, send email to sage-devel@googlegroups.com. Visit this group at http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
