Stream: new members
Yakov Pechersky (Jul 26 2020 at 21:20):
I switched from a recent mathlib commit to an older one in my
leanpkg.toml, but now am getting the following error on the first line of importing:
Yakov Pechersky (Jul 26 2020 at 21:21):
Do I have to purge my
_target folder to fix this?
Kenny Lau (Jul 26 2020 at 21:27):
leanproject doesn't work:
- go to the
git reset --hard [commit SHA]
Yakov Pechersky (Jul 26 2020 at 21:27):
Yeah, ended up doing that. Thanks!
Last updated: May 18 2021 at 17:44 UTC