tuned whitespace;
authorwenzelm
Sun, 26 Oct 2025 14:20:56 +0100
changeset 83394 8026f3a3146d
parent 83393 715a6441422f
child 83395 d2a9248792cf
tuned whitespace;
src/Tools/VSCode/extension/media/main.js
src/Tools/VSCode/extension/media/sledgehammer.js
--- 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);