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/d1935603-6a61-438a-8d8a-66678c3716d3n%40googlegroups.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 [email protected]. To view this discussion visit https://groups.google.com/d/msgid/sage-devel/04502D6B-4924-4604-B5F9-A4AABF29D292%40gmail.com.
