project build workflow

Stream: condensed mathematics

[Kevin Buzzard]

What am I doing wrong? I've not looked at this project for a while and I'm now updating it on several computers. I'm on master. I do git pull which works fine, then leanproject get-m fails with

SHA b'8174bd071fddb63d1b31ea61094342a936fa106d' could not be resolved, git returned: b'8174bd071fddb63d1b31ea61094342a936fa106d missing'

so I try leanproject build and this I think changes the mathlib in _target to the commit listed in leanpkg.toml, and then it starts building mathlib from scratch, so I break out of this and type leanproject get-m and now this works (getting cache 8174bd071f, a completely different commit) and now I can build. Hmm, I've just noticed I'm not on leanproject 1.1.0 on this computer, maybe this has something to do with it; but I don't know anything about python and can never remember how to upgrade leanproject. Why can't I just do leanproject upgrade like I can do with e.g. elan? </rant>