# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1717029809 -7200
# Node ID fdc1281430ebef1580d6eb90ad1a12efbef40050
# Parent  befb2b4bffb3ffd883f34afa6c8f486babc57d93
vscode: tuned;

diff -r befb2b4bffb3 -r fdc1281430eb 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)