I fully agree with Travis. I do not see the added value of these additional tags.
On Thu, 9 May 2024 at 23:46, Travis Scrimshaw <tcscr...@gmail.com> wrote: > > I am *very* strongly opposed to these tags. Their cutoffs are arbitrary nor > they serve no useful purpose as far as I can tell. To this point, they do not > reflect the difficulty of a review; in fact, they are at best > counterproductive to finding reviewers because it might deter people from > reviewing "large" or "huge" changes as they can include lots of trivial > doctest changes. At best it is just additional clutter in all of the > information for PRs. > > From a community perspective, I feel such changes should have been brought to > the attention of sage-devel once the PR was at a positive review. > Specifically, before the PR was merged. Not everyone has time to read every > PR, and a small consensus of developers might not reflect the development > community at-large when making changes like this. > > Best, > Travis > > > On Tuesday, May 7, 2024 at 3:12:27 PM UTC+9 seb....@gmail.com wrote: >> >> Dear Sage developers, >> >> You may have noticed that since yesterday a new type of labels with the `v:` >> prefix has appeared on our PRs. These are automatically set to classify PRs >> based on their size. For more information, see #37262. >> >> Sebastian > > -- > 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/a1904934-a31f-4ce0-83c2-76cf2d1a70f1n%40googlegroups.com. -- 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/CAGEwAA%3DBaLG%2B4BfJ-qw9cJKY5x_4zKc1%2B76yF%2BNQ6MJLVV3CMw%40mail.gmail.com.
