--- 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 () {
--- a/src/Tools/VSCode/extension/src/documentation_panel.ts Sat Oct 25 19:05:32 2025 +0200
+++ b/src/Tools/VSCode/extension/src/documentation_panel.ts Sat Oct 25 19:14:51 2025 +0200
@@ -67,7 +67,7 @@
}
this._view.webview.onDidReceiveMessage(async message => {
- if (message.command === 'openFile') {
+ if (message.command === 'open_document') {
this._open_document(message.path);
}
});