--- a/src/Tools/VSCode/extension/src/file.ts Thu Mar 03 20:04:27 2022 +0100
+++ b/src/Tools/VSCode/extension/src/file.ts Thu Mar 03 20:13:43 2022 +0100
@@ -61,6 +61,8 @@
}
+/* platform path (Windows or Posix) */
+
export function platform_path(standard_path: string): string
{
var _result = []
@@ -133,7 +135,7 @@
export async function read_bytes(path: string): Promise<Buffer>
{
- return fs.readFile(path)
+ return fs.readFile(platform_path(path))
}
export async function read(path: string): Promise<string>
--- 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)
}