Closed j-loreaux closed 1 year ago
Previously, the install/project.md had been updated to Lean 4 and lake, but the menu bar on the left still linked to leanproject.md. This points the link to the correct place and removes the leanproject.md file.
install/project.md
leanproject.md
Previously, the
install/project.md
had been updated to Lean 4 and lake, but the menu bar on the left still linked toleanproject.md
. This points the link to the correct place and removes theleanproject.md
file.