diff options
author | Omer Ben-Amram <[email protected]> | 2019-12-15 14:51:57 +0000 |
---|---|---|
committer | Omer Ben-Amram <[email protected]> | 2019-12-15 14:51:57 +0000 |
commit | 324cbe839f3110bd4d51726d5a7afe29808ade02 (patch) | |
tree | c8f859c03279f290a106237a800d2c3a2b9ebfae /editors/code | |
parent | 1d9b585c62dc92889380c9ae130d15ce7f9b08d4 (diff) |
Lowercase drive letters on windows before sending to extension.
Diffstat (limited to 'editors/code')
-rw-r--r-- | editors/code/src/notifications/publish_decorations.ts | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/editors/code/src/notifications/publish_decorations.ts b/editors/code/src/notifications/publish_decorations.ts index 120eabbc6..4441e2b28 100644 --- a/editors/code/src/notifications/publish_decorations.ts +++ b/editors/code/src/notifications/publish_decorations.ts | |||
@@ -15,8 +15,7 @@ export function handle(params: PublishDecorationsParams) { | |||
15 | // Unescaped URI should be something like: | 15 | // Unescaped URI should be something like: |
16 | // file:///c:/Workspace/ra-test/src/main.rs | 16 | // file:///c:/Workspace/ra-test/src/main.rs |
17 | // RA server might send it with the drive letter uppercased, so we force only the drive letter to lowercase. | 17 | // RA server might send it with the drive letter uppercased, so we force only the drive letter to lowercase. |
18 | const uriWithLowercasedDrive = params.uri.substr(0, 8) + params.uri[8].toLowerCase() + params.uri.substr(9); | 18 | return unescapedUri === params.uri |
19 | return unescapedUri === uriWithLowercasedDrive | ||
20 | } | 19 | } |
21 | ); | 20 | ); |
22 | 21 | ||