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/da618d46-fee1-46cd-abd6-6f144bd1319fn%40googlegroups.com.
