Zulip Chat Archive
Stream: sphere eversion
Topic: Bumping Mathlib
Oliver Nash (Oct 18 2021 at 11:44):
I had some key PRs land in Mathlib this morning. Any objections to bumping Mathlib now? @Floris van Doorn @Patrick Massot
Patrick Massot (Oct 18 2021 at 11:45):
No objection
Oliver Nash (Oct 18 2021 at 11:50):
OK done (hope that's OK Floris).
Floris van Doorn (Oct 18 2021 at 13:16):
Yes, feel free to bump mathlib whenever you want. I try to push my changes frequently to limit the scope of merge conflicts.
Last updated: Dec 20 2023 at 11:08 UTC