Skip to content

chore: bump to mathlib 4.27.0#531

Closed
grunweg wants to merge 1 commit intomasterfrom
bump
Closed

chore: bump to mathlib 4.27.0#531
grunweg wants to merge 1 commit intomasterfrom
bump

Conversation

@grunweg
Copy link
Collaborator

@grunweg grunweg commented Jan 26, 2026

No description provided.

@fpvandoorn
Copy link
Owner

Duplicate of #530 ?

@fpvandoorn fpvandoorn closed this Jan 28, 2026
@grunweg grunweg deleted the bump branch January 28, 2026 14:29
@grunweg
Copy link
Collaborator Author

grunweg commented Jan 28, 2026

Indeed, as I saw shortly after making this branch. I forgot to close the PR, though!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants