I see! On the other hand, you do benefit from this bot action after pushing changes to a non-draft PR (which probably happens much more often). But more importantly, if we disable this action, it would be a regression for developers who cannot set labels themselves.
Kwankyu Lee schrieb am Montag, 5. August 2024 um 03:49:22 UTC+2: > On Sunday, August 4, 2024 at 9:48:55 PM UTC+9 seb....@gmail.com wrote: > > We've already discussed this here: > https://github.com/sagemath/sage/pull/36213#issuecomment-1711595430 and > Tobias made a good argument for leaving it as is in > https://github.com/sagemath/sage/pull/36213#issuecomment-1711640422. > > > Once positively reviewed, we usually leave it to the author to keep the PR > branch in good state to be merged with the develop branch. This is like > "checking galley proof" stage of publishing a research paper. > > > What was the reason for rebasing a positively reviewed PR? > > > To see if the PR branch still work with the new develop branch (by running > checks all again). > > -- 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/566b1fdc-5064-4e5f-8950-302b1016c3edn%40googlegroups.com.
