diff options
Diffstat (limited to 'editors')
-rw-r--r-- | editors/code/src/commands/apply_source_change.ts | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/editors/code/src/commands/apply_source_change.ts b/editors/code/src/commands/apply_source_change.ts index 10dbf72c0..d96ace979 100644 --- a/editors/code/src/commands/apply_source_change.ts +++ b/editors/code/src/commands/apply_source_change.ts | |||
@@ -26,7 +26,8 @@ export async function handle(change: SourceChange) { | |||
26 | const toReveal = change.cursorPosition; | 26 | const toReveal = change.cursorPosition; |
27 | await vscode.workspace.applyEdit(wsEdit); | 27 | await vscode.workspace.applyEdit(wsEdit); |
28 | if (toOpen) { | 28 | if (toOpen) { |
29 | const doc = await vscode.workspace.openTextDocument(toOpen); | 29 | const toOpenUri = vscode.Uri.parse(toOpen); |
30 | const doc = await vscode.workspace.openTextDocument(toOpenUri); | ||
30 | await vscode.window.showTextDocument(doc); | 31 | await vscode.window.showTextDocument(doc); |
31 | } else if (toReveal) { | 32 | } else if (toReveal) { |
32 | const uri = Server.client.protocol2CodeConverter.asUri( | 33 | const uri = Server.client.protocol2CodeConverter.asUri( |