diff -r 81a832cab4e2 -r 669b11a039bc src/Tools/VSCode/extension/media/documentation.js --- a/src/Tools/VSCode/extension/media/documentation.js Sat Oct 25 19:05:32 2025 +0200 +++ b/src/Tools/VSCode/extension/media/documentation.js Sat Oct 25 19:14:51 2025 +0200 @@ -75,7 +75,7 @@ } else { selectedEntry = entryItem; entryItem.classList.add("selected"); - openFile(entry.path); + open_document(entry.path); } }); @@ -91,8 +91,8 @@ container.appendChild(list); } - function openFile(filePath) { - vscode.postMessage({ command: "openFile", path: filePath }); + function open_document(path) { + vscode.postMessage({ command: "open_document", path: path }); } window.onload = function () {