Accidentally editing core files causing large recompile

Stream: general

[Keefer Rowan]

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]

After the ctrl-z you can ctrl-shift-p : restart Lean. That will save you the recompilation.

[Johan Commelin]

Also, you can set the --old flag for the lean server, and it will ignore such changes and use old oleans anyway.