max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(emacs/lean-mode): lean-execute: don't clobber compile-command

Browse source
This commit is contained in:
Sebastian Ullrich 2017-07-07 17:19:23 +02:00
parent 2bfdcc9069
commit aaa59085b3
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/emacs/lean-mode.el
View file

@ -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)