leanproject get vs git clone

Stream: new members

[ZainAK283]

What's the difference between, say:
leanproject get lftcm2020
vs
git clone git@github.com:leanprover-community/lftcm2020?

[Kenny Lau]

@ZainAK283 the former downloads the oleans (compiled lean files) as well

[ZainAK283]

So in general I should do the former when possible?

[Kenny Lau]

right

[Kevin Buzzard]

The difference is that if you fire up VS Code afterwards and open a file in the repo, then you have a 1 hour wait if you used git clone, until the orange bars go away and Lean starts responding to keypresses.