From c12ea258e3a0790fec479d8199077dfcb075ff7c Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 23 Aug 2024 13:35:39 +0200
Subject: [PATCH] Test to fix backslash in URI

---
 vscode-lean4/src/utils/exturi.ts | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts
index 5ec3501b..a731bab9 100644
--- a/vscode-lean4/src/utils/exturi.ts
+++ b/vscode-lean4/src/utils/exturi.ts
@@ -10,6 +10,8 @@ export class FileUri {
     fsPath: string
 
     constructor(fsPath: string) {
+        // TODO: Is this robust on Windows???
+        fsPath = fsPath.replaceAll('\\', '/')
         this.scheme = 'file'
         this.fsPath = fsPath
     }