diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index c759e93ae..bf4a712b3 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -39,7 +39,10 @@
 
 (defun lean-execute (&optional arg)
   "Execute Lean in the current buffer"
-  (interactive "sarg: ")
+  (interactive)
+  (setq arg (concat (lean-option-string) " " arg))
+  (when (called-interactively-p)
+    (setq arg (read-string "arg: " arg)))
   (let ((target-file-name
          (or
           (buffer-file-name)