src/Tools/VSCode/extension/media/sledgehammer.js
changeset 83394 8026f3a3146d
parent 83369 8696fb442049
child 83395 d2a9248792cf
--- 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);