Closed madmini closed 3 months ago
Fixes #1357
I do not have prior experience with VSCode extensions so please check that this does not break anything. I have tested it in VSCode 1.90.2 and Theia IDE 1.50.100.
Many thanks. It looks alright to me.
Fixes #1357
I do not have prior experience with VSCode extensions so please check that this does not break anything. I have tested it in VSCode 1.90.2 and Theia IDE 1.50.100.