Keefer Rowan (Jun 02 2020 at 14:43):
How do I prevent myself from accidentally changing files like order/lattice.lean when I'm looking at them in VS Code. I'll be look through them and accidentally hit the wrong key. I quickly hit
ctrl-z but that doesn't stop VS Code from recompile a whole bunch of stuff that then takes forever. Any suggestions?
Johan Commelin (Jun 02 2020 at 14:45):
ctrl-z you can
ctrl-shift-p : restart Lean. That will save you the recompilation.
Johan Commelin (Jun 02 2020 at 14:46):
Also, you can set the
--old flag for the lean server, and it will ignore such changes and use old oleans anyway.
Last updated: May 08 2021 at 04:14 UTC