vscode: tuned;
authorThomas Lindae <thomas.lindae@in.tum.de>
Thu, 30 May 2024 02:43:29 +0200
changeset 81048 fdc1281430eb
parent 81047 befb2b4bffb3
child 81049 45ef41e823f7
vscode: tuned;
src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu May 30 02:43:24 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Thu May 30 02:43:29 2024 +0200
@@ -198,8 +198,8 @@
     language_client.onReady().then(() =>
     {
       context.subscriptions.push(
-        window.onDidChangeActiveTextEditor(_ => update_caret()),
-        window.onDidChangeTextEditorSelection(_ => update_caret()))
+        window.onDidChangeActiveTextEditor(update_caret),
+        window.onDidChangeTextEditorSelection(update_caret))
       update_caret()
 
       language_client.onNotification(lsp.caret_update_type, goto_file)