Why should a PR go automagically (!) from needs work to needs review after a merge?
Martin On Monday, 1 September 2025 at 17:38:35 UTC+2 [email protected] wrote: > On Mon, Sep 01, 2025 at 04:45:01AM -0700, 'Martin R' via sage-devel wrote: > > The problem is that the bot turns tickets from "needs work" to "needs > > review". > > It's not easy to tell a merge which doesn't fix "needs work" from one > that does. > > One way to deal with this is to mark long-time "needs work" PRs as > Draft. > (That's a "native" GitHub way to mark PRs which are not ready) > > > > > 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 > . > > -- 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/48f22a66-7915-4593-86e5-68d95827cb4an%40googlegroups.com.
