--- a/src/Tools/VSCode/extension/media/main.js Sun Oct 26 14:06:31 2025 +0100
+++ b/src/Tools/VSCode/extension/media/main.js Sun Oct 26 14:20:56 2025 +0100
@@ -3,10 +3,7 @@
for (const link of document.querySelectorAll('a[href^="file:"]')) {
link.addEventListener('click', () => {
- vscode.postMessage({
- command: "open",
- link: link.getAttribute('href'),
- });
+ vscode.postMessage({ command: "open", link: link.getAttribute('href') });
});
}
--- a/src/Tools/VSCode/extension/media/sledgehammer.js Sun Oct 26 14:06:31 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js Sun Oct 26 14:20:56 2025 +0100
@@ -72,11 +72,7 @@
history = history.filter(h => h !== item);
renderDropdown(false);
showDropdown();
-
- vscode.postMessage({
- command: 'delete_prover_history',
- entry: item
- });
+ vscode.postMessage({ command: 'delete_prover_history', entry: item });
});
row.appendChild(delBtn);