# HG changeset patch
# User wenzelm
# Date 1761232479 -7200
# Node ID 5ab0fc66e82760d6458929efc2e1f71ccd8b9ed5
# Parent  9252ebcd1fb51889e45a664e26a3bac7238a28ef
tuned comments;

diff -r 9252ebcd1fb5 -r 5ab0fc66e827 src/Tools/VSCode/extension/media/symbols.js
--- a/src/Tools/VSCode/extension/media/symbols.js	Thu Oct 23 17:02:07 2025 +0200
+++ b/src/Tools/VSCode/extension/media/symbols.js	Thu Oct 23 17:14:39 2025 +0200
@@ -238,7 +238,7 @@
 
         const button = document.createElement('div');
         if (group === "arrow") {
-          button.classList.add('arrow-button'); // Spezielle Klasse für Pfeile
+          button.classList.add('arrow-button'); // special class for arrows
         } else {
           button.classList.add('symbol-button');
         }