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 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/a58f6121-5c30-4be0-bf2a-cdea0193bd8dn%40googlegroups.com.