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

*Sorry, typo in the headline: July -> June!* seb@gmail.com schrieb am Freitag, 7. Juni 2024 um 23:49:54 UTC+2: > Dear Sage developers, > > We will now continue with a process that started last July > . > Unfortunately, thi

[sage-devel] Synchronization of GitHub state and priority labels continues on Tuesday July 11th

Dear Sage developers, We will now continue with a process that started last July . Unfortunately, this was blocked for many months while we waited for GitHub to fix a bug in their web-interface. Although this bug is still not

Re: [sage-devel] Re: New labels v: mimimal, v: small ... on pull requests

*> How about having a voting for this issue? * Another possibility would be to have a blacklist (but I don't know where) that developers can sign up to if they want to be excluded from automations that apply to PRs. In this thread's example, a developer would exclude PRs that he himself author

[sage-devel] Re: New labels v: mimimal, v: small ... on pull requests

*> (Note that only members of the Triage team can set the "needs review" label.)* See this comment in #35927 for a suggestion to solve this. Matthias Koeppe schrieb am Dienstag, 28. Mai 2024 um 21:35:26 UTC+2: > I'll ex