On Wednesday, October 2, 2024 at 1:57:48 AM UTC-7 Dima Pasechnik wrote: > And for sure doing any such renaming games will be outside of the scope of the PR in question. https://github.com/sagemath/sage/pull/36380 should not wait for it.
#36380 is first of all waiting for, requested by more than one reviewer, splitting off the part related to brial - as the latter is a really urgent and unrelated to sagemath-categories thing. I have already corrected you about this; why repeat it? It's not "unrelated" to sagemath-categories. sagemath-brial needs a larger sagemath-categories as a build dependency. -- 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/82d269aa-928e-475d-9d54-766883518235n%40googlegroups.com.
