| Wed, 17 Jul 2024 21:03:56 +0200 | Thomas Lindae | vscode: removed unused code; | file | diff | annotate |
| Wed, 12 Jun 2024 20:54:11 +0200 | Thomas Lindae | vscode: added all fonts to extension; | file | diff | annotate |
| Mon, 27 May 2024 13:20:31 +0200 | Thomas Lindae | vscode: IsabelleDejaVuSansMono for state and output panel; | file | diff | annotate |
| Mon, 21 Mar 2022 11:40:11 +0100 | wenzelm | clean build from explicit MANIFEST: avoid accidental garbage in vsix package; | file | diff | annotate |