# HG changeset patch
# User wenzelm
# Date 1761415941 -7200
# Node ID 05abe5a82410840f844924e4e0de18d5a7e90aad
# Parent  8d9c494b78cf110e299b6f20750585edd5d05ee4
tuned whitespace;

diff -r 8d9c494b78cf -r 05abe5a82410 src/Tools/VSCode/extension/media/documentation.js
--- 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);
+      }
+    };
   })();