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

fix(emacs/lean-mode): handle when there is spaces in filenames

Browse source
This commit is contained in:
Soonho Kong 2014-11-04 19:22:35 -05:00
parent 53e18d0e39
commit 2273f75e9b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -32,7 +32,7 @@
(defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and file-name"
(format "%s %s %s" exe-name args file-name))
(format "\"%s\" %s \"%s\"" exe-name args file-name))
(defun lean-create-temp-in-system-tempdir (file-name prefix)
"Create a temp lean file and return its name"