The problem is that the bot turns tickets from "needs work" to "needs review".
On Monday, 1 September 2025 at 01:07:41 UTC+2 [email protected] wrote: > Technically speaking, merging a branch into PR might lead to breaking > changes. > So it's a grey zone. > > I would say, if the branch status says that the base branch is outdated, > but "changes can be cleanly merged", there is no pressing need to do this > merge. And if you do the merge please at least check that the CI continues > to be OK. Often it's safe to turn the positive review status back on after > this. > > > > On August 31, 2025 5:31:48 AM CDT, 'Martin R' via sage-devel < > [email protected]> wrote: > >> Ii is currently a pain to find pull requests that *really* need review, >> because, after every minor release, people tend to merge develop (which >> makes sense), and then some bot changes the label to "needs review", no >> matter what it was before. >> >> Can somebody please please fix that? >> >> Martin >> >> -- 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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/sage-devel/a86c786d-7c06-48ba-a565-21ebc69b890cn%40googlegroups.com.
