Closed RalfJung closed 3 weeks ago
There also doesn't seem to be a way to use vscode settings to hide these icons per workspace, unfortunately.
I am surprised it is not already the case :sweat: I will take care of it !
I should have mentioned: this is with v2.1.7 of the extension.
Ever since I installed vscoq, the Coq icon shows up in the sidebar in all vscodium windows -- whether I do Rust, LaTeX, whatever, the Coq icon is always there:
Other extensions generally hide themselves when they are not relevant for the current window (e.g. the LaTeX extension). Would be nice if vscoq could do the same. :)