Zulip Chat Archive
Stream: Infinity-Cosmos
Topic: Mathlib Bump
Pietro Monticone (Nov 12 2024 at 21:03):
Manual intervention required for cosmos#42.
Note: The InfinityCosmos project has been "linkified." Use the command cosmos#ISSUE_NUMBER to link directly to the relevant issue or PR.
Last updated: May 02 2025 at 03:31 UTC