move selections

hhu-adam · Jul 22, 2024 · 9ca54f1 · 9ca54f1
1 parent 99ee38b
commit 9ca54f1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
@@ -89,7 +89,7 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource {
     }
 
     selectionMoveMode(): SelectionMoveMode {
-        return { kind: 'OnlyMoveCursorSelections', updateUnchangedSelections: this.isVimExtensionInstalled }
+        return { kind: 'MoveAllSelections' }
     }
 
     collectSelections(): Range[] {