diff -r 715a6441422f -r 8026f3a3146d src/Tools/VSCode/extension/media/sledgehammer.js --- 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);