Closed fpvandoorn closed 4 months ago
The old version of lake creates a wrong .gitignore.
.gitignore
Alternatively, we use the instructions from the wiki:
lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math
but that will require an elan self update first for many users (including me).
elan self update
The old version of lake creates a wrong
.gitignore
.Alternatively, we use the instructions from the wiki:
but that will require an
elan self update
first for many users (including me).