> Note that "github-actions[bot]" in Reviewers. What does this mean? I don't understand how this happened... > > Could this be somehow related with the recent synchronization turn-on?
Yes, since the GitHub state request-changes was not set before you add the s: needs work label the bot sets it for you. Of course it would be much nicer if the bot would set your name into the reviewer field (making the comment indeed redundant). But, this seems to be impossible (even via the REST API). At the moment the labeled-trigger is disabled again by reasons indicated in Dima's post (for more information see this comment in #36177 <https://github.com/sagemath/sage/pull/36177#issuecomment-1704022893> and the following). I've opened PR #36213 <https://github.com/sagemath/sage/pull/36213> to treat issues that have been observed in connection with the labeled event. Kwankyu Lee schrieb am Sonntag, 3. September 2023 um 14:28:43 UTC+2: > Note that "github-actions[bot]" in Reviewers. What does this mean? I don't > understand how this happened... > > Could this be somehow related with the recent synchronization turn-on? > > > ____________________________________________________________________________ > > [image: Screenshot 2023-09-03 at 9.23.20 PM.png] > > On Sunday, September 3, 2023 at 2:54:20 PM UTC+9 Kwankyu Lee wrote: > >> Thanks. >> >> I noticed one defect (nothing serious). For "closed" event, the message >> is succinct. >> ------------------------------------------- >> >> [image: Screenshot 2023-09-03 at 2.43.25 PM.png] >> ------------------------------------------- >> Now for adding status label ("s: needs work"), the message is >> ------------------------------------------- >> [image: Screenshot 2023-09-03 at 2.48.07 PM.png] >> ------------------------------------------- >> I think this is too verbose. In particular, the message "kwankyu >> requested changes for this PR" is redundant. >> > -- 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/d8783c93-d1e2-4c20-b705-46622139b7c8n%40googlegroups.com.
