VSCode not showing errors

Stream: maths

[Bhavik Mehta]

VS code isn't showing red underlines for errors for me, even though the problems bar at the bottom does and I'm getting lean errors on the right

[Bhavik Mehta]

Restarting lean doesn't fix it

[Bhavik Mehta]

Oh it's back now... how confusing!

[Bryan Gin-ge Chen]

Very odd. If you can figure out how to reproduce this, please create an issue at the vscode-lean repo. (Also, I'm not sure this thread should be in #maths)

[Bhavik Mehta]

Will do! (Sorry, my mistake - meant to put it in #new members and must have missed somehow!)

[Gabriel Ebner]

Did you use the git extension to revert a change, etc.?

[Bhavik Mehta]

Nope

[Gabriel Ebner]

I have also run into this issue. Most often it happens when I revert a change. Sometimes it helps to just close the current file and open it again.