leanproject get-m --rev

Stream: general

[Bolton Bailey]

I was working with my mentee today and I was surprised to see that when I had him use leanproject get-m --rev origin/master, he got an error message, saying that this command had no --rev option. leanproject get-m -h confirmed this. He was using leanproject, version 1.1.0, whereas I use leanproject, version 1.0.0. DId something change between these versions to remove this option? How can I get this effect with this version of leanproject?

[Eric Wieser]

Use get-c not get-m

[Eric Wieser]

get-cache means "get the cache for the current lean project" (aka consult azure if the current project is mathlib, else look for a cache locally)

[Eric Wieser]

get-mathlib-cache means "get a fresh copy of mathlib in my _target directory of some non-mathlib project"