[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 > >