On Saturday, July 27, 2024 at 6:01:48 PM UTC+9 Martin R wrote:
I think it would be good to have a conscious decision about when a merge of this pull request should happen. Since it affects 2262 (!) files, just about everybody will have to rebase their work. Also, when there is a clear decision, the author will not have to fix merge conflicts again and again. git is smart and the author is skillful in git. I look forward a good luck in the next release :-) -- 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/df776ae0-9e3e-417d-aa3d-5316ef63b906n%40googlegroups.com.
