| 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);