VSCode Explorer colors and Git

Stream: general

[Pieter Cuijpers]

Silly "how to use VSCode" question that some of you probably already ran into...

I've moved my first tries in Lean4 to a git repository, and now VSCode has decided to change the way it colours the files in the explorer overview. I found a way to "disable" git decorations, but this does not bring back the nice "green filenames" when a file typechecks correctly.
I suspect this is just a setting that you have to know where to look for...

Ideas anyone?

[Pedro Sánchez Terraf]

Yes, I also miss green :sad: I'm on Lean 3 though

[Patrick Stevens]

You could entirely turn off Git integration, if it's coming through the Git extension? Search VSCode's settings for "git.enabled" and set it to false?

[Patrick Stevens]

(haven't tried it myself, might not work)

[Trebor Huang]

This is done by workspace.FileDecoration in VSCode I think, a quick scan seems to suggest the Lean 4 VSCode extension doesn't have that function yet.