[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

I don't understand what you mean here. Can you please explain this in the new PR. Kwankyu Lee schrieb am Montag, 18. September 2023 um 03:17:50 UTC+2: > In a message of > https://github.com/sagemath/sage/pull/36020#issuecomment-1722629380, > please change to "state label" (or "status label"

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

Yes. This will be done in PR #36292 . Kwankyu Lee schrieb am Montag, 18. September 2023 um 03:07:14 UTC+2: > On Friday, September 8, 2023 at 5:47:30 PM UTC+9 seb@gmail.com wrote: > > > I think this is too verbose. In particular, the message

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

See the comment in #36213 . Kwankyu Lee schrieb am Montag, 18. September 2023 um 03:03:26 UTC+2: > For a case where it's not done cleanly, see > >

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

In a message of https://github.com/sagemath/sage/pull/36020#issuecomment-1722629380, please change to "state label" (or "status label" which I prefer) from "state-label". -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

On Friday, September 8, 2023 at 5:47:30 PM UTC+9 seb@gmail.com wrote: > I think this is too verbose. In particular, the message "kwankyu requested changes for this PR" is redundant. >From the point of view of a developer familiar with Trac status labels, I agree. However, a key goal of

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

For a case where it's not done cleanly, see https://github.com/sagemath/sage/pull/36020#issuecomment-1722629380 -- 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] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

> 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

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

> I think this is too verbose. In particular, the message "kwankyu requested changes for this PR" is redundant. >From the point of view of a developer familiar with Trac status labels, I agree. However, a key goal of the GitHub migration was to attract new developers who are familiar with the

Re: [sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

well, obviously such a bot needs some sort of permissions. The present problem with this is also with permissions - reviews from non-admins are just comments, from GitHub's point of view, and in our development model this is not what's needed. On Sun, 3 Sept 2023, 15:28 Kwankyu Lee, wrote: >

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

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

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

Tobias activated the functionality today (see https://github.com/sagemath/sage/issues/35927#issuecomment-1703696369). Kwankyu Lee schrieb am Freitag, 1. September 2023 um 22:36:56 UTC+2: > How is this going? > > On Friday, August 4, 2023 at 1:54:13 AM UTC+9 seb@gmail.com wrote: > >> I've

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

How is this going? On Friday, August 4, 2023 at 1:54:13 AM UTC+9 seb@gmail.com wrote: > I've added a comment > > to issue #35927 to enable > a next step accordingly.

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

I've added a comment to issue #35927 to enable a next step accordingly. More information about what will change in this step can be found there. Kwankyu Lee schrieb am

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

Personally, I want the feature to keep at most one status(state) label for a PR, so that if a person add a new status label (say "positive review"), then the old one ("needs review") is automatically removed. Currently it is annoying to do this manually. -- You received this message because

[sage-devel] Re: Synchronization of GitHub state and priority labels starts on Tuesday July 18th

Look at the action of the synchronization workflow in the recently merged PR https://github.com/sagemath/sage/pull/35997 (the last part). The workflow works well on the close event! On Tuesday, July 11, 2023 at 4:08:40 PM UTC+9 seb@gmail.com wrote: > Dear Sage developers, > > > Now, it's