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