Another data point: the bot is getting the size wrong too:
https://github.com/sagemath/sage/pull/38105
I *very* strongly believe we should disable this automatically being added
to PRs.
Travis
On Friday, May 10, 2024 at 3:21:57 PM UTC+9 seb@gmail.com wrote:
> I must confess that I have no
I *very* strongly believe we should disable this automatically being added
to PRs.
How about having a voting for this issue?
--
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, s
On Tuesday, May 28, 2024 at 1:24:17 AM UTC-7 Travis Scrimshaw wrote:
Another data point: the bot is getting the size wrong too:
https://github.com/sagemath/sage/pull/38105
Thanks, I've let the author know
in https://github.com/sagemath/sage/pull/37262#issuecomment-2135699139
--
You receive
I'll expand a little bit, in the hope to stimulate a constructive
discussion. (A previous related
thread: https://groups.google.com/g/sage-devel/c/sulCa-6EZRA/m/86jFAw9NAAAJ)
There is a very serious, project-level concern: Is our project welcoming to
new contributors?
We tell contributors to g
