Properly use (interactive)

leanprover-community · Dec 12, 2024 · 1754b21 · 1754b21
1 parent f0eeac6
commit 1754b21
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/lean4-mode.el b/lean4-mode.el
@@ -92,9 +92,7 @@ FILE-NAME."
 
 (defun lean4-execute (&optional arg)
   "Execute Lean in the current buffer with an optional argument ARG."
-  (interactive)
-  (when (called-interactively-p 'any)
-    (setq arg (read-string "arg: " arg)))
+  (interactive "sArgument to Lean4 executable: ")
   (let* ((use-lake (lean4-lake-find-dir))
          (default-directory (if use-lake (lean4-lake-find-dir)
                               default-directory))