How to get _target directory after checking out from github?

Stream: new members

[Martin C. Martin]

I did a fresh checkout of my project from github. It has a leanpkg.toml file describing a dependency on mathlib. How do I check this out, i.e. _target/deps directory that contains the specified version of mathlib?

[Kevin Buzzard]

leanproject get-mathlib

[Patrick Massot]

This shouldn't be necessary if you use leanproject get username/projectname to get the project from GitHub.

[Martin C. Martin]

Oh interesting, thanks!