I vote for (A1) and no other option. (I don't see enough added value of these labels and I think that any *list approach is going to be a too obscure feature to warrant the extra effort of maintaining it.)
On Thursday, June 13, 2024 at 6:27:46 AM UTC+3 tcsc...@gmail.com wrote: > PR labels are being automatically added to roughly indicate their size. > There are three options besides keeping the current behavior: > > (A1) Remove the automatic adding of labels; the must be added manually > (like most other labels). > (A2) Have a "whitelist" of contributors who want to have this > automatically added to their PRs. > (A3) Have a "blacklist" of contributors who do not want to have this > automatically added to their PRs. > (B) Keep the current way of automatically adding it for all PRs. > > This will be assuming that if you vote for (Ai), your vote will > automatically count for all (Aj) >= (Ai) unless you state otherwise. For > example, if there are 3 votes for (A1), 2 votes for (A3) and 4 votes for > (B), we will go with (A3) as the total is 5 votes. > > The vote will close on *Friday, June 21st*. > > For the discussion, see: > https://groups.google.com/g/sage-devel/c/w4IeYgXgVUc/m/nV-ZT9BpAgAJ > > My vote: (A1) > > Best, > Travis > -- 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/1c911ca3-ae3d-4d83-aa96-f3369a3467ffn%40googlegroups.com.