# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1715724694 -7200
# Node ID 07ed4ce5c6c99025b7c7e49bec90ac8d37cd57d9
# Parent  f1aef71103296af14ce35d8a8189cea90f182e9d
vscode: changed test_string to "mix" to be consistent with jEdit;

diff -r f1aef7110329 -r 07ed4ce5c6c9 src/Tools/VSCode/extension/media/main.js
--- a/src/Tools/VSCode/extension/media/main.js	Thu May 16 12:00:05 2024 +0200
+++ b/src/Tools/VSCode/extension/media/main.js	Wed May 15 00:11:34 2024 +0200
@@ -26,7 +26,7 @@
         });
 
     const get_window_margin = () => {
-        const test_string = "a";
+        const test_string = "mix";
         const test_span = document.createElement("span");
         test_span.textContent = test_string;
         document.body.appendChild(test_span);