diff options
author | Omer Ben-Amram <[email protected]> | 2019-12-15 15:10:39 +0000 |
---|---|---|
committer | Omer Ben-Amram <[email protected]> | 2019-12-15 15:10:39 +0000 |
commit | 75353753cdcb993c277ce1d8bb366c708eabe2c6 (patch) | |
tree | fad356cd7a69e7da8367334adf127773015212ba /editors/code | |
parent | ebf302d2610527c35b8fb794a03cc1c280c8a9d3 (diff) |
`npm run fix`
Diffstat (limited to 'editors/code')
-rw-r--r-- | editors/code/src/notifications/publish_decorations.ts | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/editors/code/src/notifications/publish_decorations.ts b/editors/code/src/notifications/publish_decorations.ts index 2ccd2d585..f23e286ad 100644 --- a/editors/code/src/notifications/publish_decorations.ts +++ b/editors/code/src/notifications/publish_decorations.ts | |||
@@ -9,14 +9,12 @@ export interface PublishDecorationsParams { | |||
9 | } | 9 | } |
10 | 10 | ||
11 | export function handle(params: PublishDecorationsParams) { | 11 | export function handle(params: PublishDecorationsParams) { |
12 | const targetEditor = vscode.window.visibleTextEditors.find( | 12 | const targetEditor = vscode.window.visibleTextEditors.find(editor => { |
13 | editor => { | 13 | const unescapedUri = unescape(editor.document.uri.toString()); |
14 | const unescapedUri = unescape(editor.document.uri.toString()); | 14 | // Unescaped URI looks like: |
15 | // Unescaped URI looks like: | 15 | // file:///c:/Workspace/ra-test/src/main.rs |
16 | // file:///c:/Workspace/ra-test/src/main.rs | 16 | return unescapedUri === params.uri; |
17 | return unescapedUri === params.uri | 17 | }); |
18 | } | ||
19 | ); | ||
20 | 18 | ||
21 | if (!Server.config.highlightingOn || !targetEditor) { | 19 | if (!Server.config.highlightingOn || !targetEditor) { |
22 | return; | 20 | return; |