Zulip Chat Archive
Stream: PR reviews
Topic: simplify lakefile post_update hook #21650
Kim Morrison (Feb 16 2025 at 22:14):
#21650 removes a now redundant step of the post_update hook in the Mathlib lakefile. Would someone be able to take a look?
Last updated: May 02 2025 at 03:31 UTC