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'); }