tuned whitespace;

--- a/src/Tools/VSCode/extension/media/documentation.js	Sat Oct 25 20:09:37 2025 +0200
+++ b/src/Tools/VSCode/extension/media/documentation.js	Sat Oct 25 20:12:21 2025 +0200
@@ -80,9 +80,9 @@
     }
 
     window.onload = function () {
-        const state = vscode.getState();
-        if (state && state.sections) {
-          update(state.sections);
-        }
-      };
+      const state = vscode.getState();
+      if (state && state.sections) {
+        update(state.sections);
+      }
+    };
   })();