From aaa59085b311463c8ac6188fd243e2e4131cbcf4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 7 Jul 2017 17:19:23 +0200 Subject: [PATCH] fix(emacs/lean-mode): lean-execute: don't clobber compile-command --- src/emacs/lean-mode.el | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index adbdd8e4bc..b9ae2bdfea 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -48,14 +48,17 @@ (interactive) (when (called-interactively-p 'any) (setq arg (read-string "arg: " arg))) - (let ((target-file-name + (let ((cc compile-command) + (target-file-name (or (buffer-file-name) (flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir)))) (compile (lean-compile-string (shell-quote-argument (f-full (lean-get-executable lean-executable-name))) (or arg "") - (shell-quote-argument (f-full target-file-name)))))) + (shell-quote-argument (f-full target-file-name)))) + ;; restore old value + (setq compile-command cc))) (defun lean-std-exe () (interactive)