src/Tools/VSCode/extension/src/symbol.ts

--- a/src/Tools/VSCode/extension/src/symbol.ts	Fri Mar 11 09:23:05 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Mon Mar 14 16:03:15 2022 +0100
@@ -81,7 +81,7 @@
 {
   const vscodium_home = library.getenv("ISABELLE_VSCODIUM_HOME")
   if (vscodium_home) {
-    const path = vscodium_home + "/resources/app/out/vs/base/browser/ui/fonts/symbols.json"
+    const path = vscodium_home + "/resources/vscodium/out/vs/base/browser/ui/fonts/symbols.json"
     return file.read_json_sync(file.platform_path(path))
   }
   else { return [] }