michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(emacs/lean-mode): lean-execute

Browse source 
shell-quote-argument also escapes '~' into '\~' which causes a problem.
This fix first calls 'f-full' to get a absolute path, then call
shell-quote-argument.

close #544
This commit is contained in:
Soonho Kong 2015-04-17 00:24:42 +01:00
parent 2e675c1bdd
commit 3d79f89f5e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,9 +49,9 @@
(buffer-file-name)
(flymake-init-create-temp-buffer-copy 'lean-create-temp-in-system-tempdir))))
(compile (lean-compile-string
(shell-quote-argument (lean-get-executable lean-executable-name))
(shell-quote-argument (f-full (lean-get-executable lean-executable-name)))
(or arg "")
(shell-quote-argument target-file-name)))))
(shell-quote-argument (f-full target-file-name))))))
(defun lean-exec-at-pos (process-name process-buffer-name &rest options)
"Execute Lean by providing current position with optional