Deselect everything

Stream: lean4

[Patrick Massot]

Do we have a short-cut to de-select everything in the infoview in VSCode? If no, would it be easy to add? @Marc Huisinga @Wojciech Nawrocki

[Wojciech Nawrocki]

Ah no, even the reload button doesn't seem to do it. It shouldn't be too difficult, but could you please make a brief feature request issue on vscode-lean4?

[Patrick Massot]

I opened https://github.com/leanprover/vscode-lean4/issues/378