Skip to content

Pin mathlib4 to port-complete#252

Open
eric-wieser wants to merge 4 commits intomasterfrom
port-complete-branch
Open

Pin mathlib4 to port-complete#252
eric-wieser wants to merge 4 commits intomasterfrom
port-complete-branch

Conversation

@eric-wieser
Copy link
Member

This is not intended for merging into master.

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.

1 participant