Possible bug with lake update

Stream: lean4

[Tomaz Gomes Mascarenhas]

Hi, I don't think the behavior of lake update is correct in the following case:

• Create new project with lake new test
• Change lakefile.lean to import std4
• Run lake update to clone std4 into ./lean_packages
• Change lakefile.lean to import mathlib4
• Run lake update to clone mathlib4 into ./lean_packages

this last command returns the following error:
error: cannot find revision master in repository ./lean_packages/std

[Gabriel Ebner]

If you still have the lean_packages directory then you have an old version of Lake/Lean. Please upgrade Lean. (if you depend on mathlib4, then you should use the same version as mathlib4)