Zulip Chat Archive
Stream: mathlib4
Topic: updating lean-toolchain on update
Ruben Van de Velde (Dec 01 2024 at 07:28):
Given lean4#5684 (which landed in v4.14.0-rc3), can we remove the post-update script in mathlib's lakefile?
Kim Morrison (Dec 01 2024 at 08:17):
Yes, I think so!
Last updated: May 02 2025 at 03:31 UTC