On Tuesday, May 28, 2024 at 12:19:42 PM UTC-7 Matthias Koeppe wrote: 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 His PR https://github.com/sagemath/sage/pull/38114 fixes the size computation for PRs that are based on an out-of-date base branch. -- 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/c7192b5e-0bde-44df-8f83-2d531b775bcen%40googlegroups.com.
