vscode-lean4 icon indicating copy to clipboard operation
vscode-lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

feat: [lean4web] add option to change selectionMoveMove

Open abentkamp opened this issue 1 year ago • 0 comments
trafficstars

The selections don't move correctly when using monaco editor. This PR allows us to switch the selection move mode. The functionality of the VSCode extension is unchanged.

abentkamp avatar Jul 22 '24 13:07 abentkamp