VS Code: only report errors/warning in current file

Stream: general

[Kevin Buzzard]

I have 10 lean files open, I'm manually porting some basic logic exercises from lean 3 to lean 4. It's really annoying that I can't look at the bottom blue line and answer the question "has this file currently got no warnings and errors?" because all the warnings in the question files which are (supposed to be) full of sorrys and all the errors in the lean 3 files being compiled as lean 4 files because I haven't finished manually fixing them up also contribute to the total.

Can I make VS Code report warnings and errors in the current visible file only?

errors.png