It really does not work this way. On Monday, July 1, 2024 at 7:21:34 PM UTC-7 Travis Scrimshaw wrote:
> Sorry for the delayed response due to conference travel. > > Vote count: > > (A1) 5 > (A3) 1 > (B) 1ish > > As such, please remove this automatic labeling of PR sizes. > > We can have a proper discussion about how to make it easier for newcommers > to find good PRs to review, but we should actually have that discussion > before adding such features. > > Best, > Travis > > On Monday, June 17, 2024 at 3:19:45 PM UTC+9 seb....@gmail.com wrote: > >> > *The feature might have been wrongly guided* >> >> I'm sorry, that was my mistake (see my recent comment >> <https://github.com/sagemath/sage/pull/37262#issuecomment-2172370992>in >> #37262 <https://github.com/sagemath/sage/pull/37262>). This caused that >> there is a difference between B and B7. >> >> > *Nevertheless, it would be very unwelcoming to just revert it.* >> >> This is the motivation behind Option A3. >> >> >> Vincent Delecroix schrieb am Samstag, 15. Juni 2024 um 08:52:00 UTC+2: >> >>> On the material side I vote (A1). >>> >>> On the human side I vote (B). Matthias raised a delicate point: this >>> feature was introduced by a newcomer to sage development. The feature >>> might have been wrongly guided or badly thought. Nevertheless, it >>> would be very unwelcoming to just revert it. >>> >>> Ideally, there would be a "make the feature even nicer" solution >>> rather than "get rid of that s***". Though, this requires a concrete >>> proposal more than a vote, and I have nothing magical to share at this >>> stage. >>> >>> Best >>> Vincent >>> >>> On Fri, 14 Jun 2024 at 13:56, Kwankyu Lee <ekwa...@gmail.com> wrote: >>> > >>> > +1 to (A1) >>> > >>> > -- >>> > 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+...@googlegroups.com. >>> > To view this discussion on the web visit >>> https://groups.google.com/d/msgid/sage-devel/cd9f975b-3605-4e98-a165-2a2e1d4ab2b9n%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/12f3ce38-7b52-4b1f-8852-c316e02105cen%40googlegroups.com.
