src/Tools/VSCode/extension/media/sledgehammer.js
changeset 83416 c7849fa2ece0
parent 83407 a51835dd6a64
child 83421 2740ae774d80
--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Mon Oct 27 12:15:14 2025 +0100
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Mon Oct 27 12:37:31 2025 +0100
@@ -190,14 +190,7 @@
 
   const locate_button = document.createElement("button");
   locate_button.textContent = "Locate";
-  locate_button.addEventListener("click", () => {
-    vscode.postMessage({
-      command: "locate",
-      provers: provers_input.value,
-      isar: isar_checkbox.checked,
-      try0: try0_checkbox.checked
-    });
-  });
+  locate_button.addEventListener("click", () => vscode.postMessage({ command: "locate" }));
 
   top_row.appendChild(provers_label);
   top_row.appendChild(isar_label);