leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
54 stars 123 forks source link

add comment about not making a new folder #380

Closed fpvandoorn closed 1 year ago

fpvandoorn commented 1 year ago

A very common mistake of new users is that they create a project folder themselves before cloning the repository. This often causes confusion in later steps (running lake exe cache get in the wrong directory, or opening the wrong directory in VSCode). I've seen new users do this on 3 different occasions now, and they got stuck at a later step.