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

--- a/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 20:04:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Thu Mar 03 20:13:43 2022 +0100
@@ -83,6 +83,6 @@
 
 export async function load_symbols(path: string): Promise<Symbols>
 {
-  const entries = await file.read_json<[Entry]>(file.platform_path(path))
+  const entries = await file.read_json<[Entry]>(path)
   return new Symbols(entries)
 }