Zulip Chat Archive
Stream: general
Topic: outdated oleans
Kenny Lau (Jul 02 2020 at 17:44):
When does VSCode use outdated oleans? I've heard that sometimes if you edit a file deep in the import hierarchy, VSCode will just give up and use the outdated oleans.
Johan Commelin (Jul 02 2020 at 17:46):
You are not talking about the --old command line option to Lean, or is that what you meant?
Kenny Lau (Jul 02 2020 at 18:21):
no, I'm not talking about --old
Last updated: Dec 20 2023 at 11:08 UTC