error while loading shared libraries

Stream: mathlib4

[Kevin Buzzard]

I just pulled mathlib4 master and typed lake build and I got

/home/buzzard/.elan/toolchains/leanprover--lean4---nightly-2022-10-20/bin/lake: error while loading shared libraries: libleanshared.so: cannot open shared object file: No such file or directory

What did I do wrong? :-(

[Kevin Buzzard]

fixed it by nuking the toolchain (I might have triggered two downloads of the toolchain simultaneously, one on the command line and one in VS Code)