From ff6862f587c09fa35501b9d6fc9d63e22e0f2172 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Mon, 15 Sep 2014 09:47:00 -0700
Subject: [PATCH] fix(emacs/lean-mode): pass lean-options to lean-execute

Related issue: #196
---
 src/emacs/lean-mode.el | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

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)