Skip to content

Conversation

@joneugster
Copy link
Member

@joneugster joneugster commented Jul 22, 2025

Once the v4.21.0 tag is available in lean4game one needs to run lake update once to change the lean4game dependency in the manifest to the non-local one.

@joneugster joneugster merged commit cc380a0 into main Aug 5, 2025
1 check passed
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.

3 participants