diff options
| author | Aleksey Kladov <[email protected]> | 2018-08-30 10:51:46 +0100 |
|---|---|---|
| committer | Aleksey Kladov <[email protected]> | 2018-08-30 10:52:21 +0100 |
| commit | 1f2fb4e27f8ba1cb7b1d96a332b7ffc2ee659921 (patch) | |
| tree | bd5c0a9b83c181fb3a906c41cbeb3ea7f63ae081 /code | |
| parent | 0d6d74e78ecb6d110de751c528e662fc61113e78 (diff) | |
move
Diffstat (limited to 'code')
| -rw-r--r-- | code/src/extension.ts | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/code/src/extension.ts b/code/src/extension.ts index f2589ef2f..53ef83aab 100644 --- a/code/src/extension.ts +++ b/code/src/extension.ts | |||
| @@ -395,7 +395,7 @@ async function applySourceChange(change: SourceChange) { | |||
| 395 | let uri = client.protocol2CodeConverter.asUri(toReveal.textDocument.uri) | 395 | let uri = client.protocol2CodeConverter.asUri(toReveal.textDocument.uri) |
| 396 | let position = client.protocol2CodeConverter.asPosition(toReveal.position) | 396 | let position = client.protocol2CodeConverter.asPosition(toReveal.position) |
| 397 | let editor = vscode.window.activeTextEditor; | 397 | let editor = vscode.window.activeTextEditor; |
| 398 | if (!editor || editor.document.uri != uri) return | 398 | if (!editor || editor.document.uri.toString() != uri.toString()) return |
| 399 | if (!editor.selection.isEmpty) return | 399 | if (!editor.selection.isEmpty) return |
| 400 | editor!.selection = new vscode.Selection(position, position) | 400 | editor!.selection = new vscode.Selection(position, position) |
| 401 | } | 401 | } |