Here I forward this post from Dima, which didn't find the right channel:
*Fri, Jun 14, 12:25 PM (3 days ago)Please record my vote for A3.I also wonder whether this setup has a side feature which would allowus to collect stats on the sizes of contributions.CheersDima* Gareth Ma schrieb am Samstag, 15. Juni 2024 um 23:35:14 UTC+2: > I vote for (A1) and no other options. > > In fact, I don't think size related labels should be a thing at all, so the > second half of (A1), i.e. "the[y] must be added manually (like most other > labels)", should preferably be removed as well. (The wording suggests they > will > be kept and added manually.) > > On 6/15/24 7:49 AM, Vincent Delecroix wrote: > > 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/7104c4c7-f403-4ebd-94a7-5dc4f1c31188n%40googlegroups.com.
