diff options
| author | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-01-15 12:10:37 +0000 |
|---|---|---|
| committer | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-01-15 12:10:37 +0000 |
| commit | 2184f7f14250c888e37cc27475c085515ea63aa4 (patch) | |
| tree | a8856fbc3179ca3f52f3b8ca00cf481954c6f351 | |
| parent | f6f2e89e7ac9c4afbda11bade21f902c552fbba2 (diff) | |
| parent | cd21f0eadead4129bc2e91434e015c660e02c880 (diff) | |
Merge #545
545: Reveal the newly added source change in the editor. r=matklad a=kjeremy
Fixes #543
Co-authored-by: Jeremy A. Kolb <[email protected]>
| -rw-r--r-- | editors/code/src/commands/apply_source_change.ts | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/editors/code/src/commands/apply_source_change.ts b/editors/code/src/commands/apply_source_change.ts index 675a534c8..389061e3c 100644 --- a/editors/code/src/commands/apply_source_change.ts +++ b/editors/code/src/commands/apply_source_change.ts | |||
| @@ -46,5 +46,6 @@ export async function handle(change: SourceChange) { | |||
| 46 | return; | 46 | return; |
| 47 | } | 47 | } |
| 48 | editor.selection = new vscode.Selection(position, position); | 48 | editor.selection = new vscode.Selection(position, position); |
| 49 | editor.revealRange(new vscode.Range(position, position), vscode.TextEditorRevealType.Default); | ||
| 49 | } | 50 | } |
| 50 | } | 51 | } |