Zulip Chat Archive

Stream: nightly-testing

Topic: nightly#87 adaptations for nightly-2025-10-11

github mathlib4 bot (Oct 11 2025 at 13:50):

chore: adaptations for nightly-2025-10-11 nightly#87 Please review this PR. At the next toolchain release this diff will land in 'master'.

Kevin Buzzard (Oct 11 2025 at 14:07):

See discussion at #nightly-testing > nightly#86 adaptations for nightly-2025-10-10 @ 💬

Kevin Buzzard (Oct 11 2025 at 14:09):

If someone sorts out this comment issue then I can merge. If I start editing the PR then someone else will have to, I guess?

Last updated: Dec 20 2025 at 21:32 UTC