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

fix(emacs/lean-mode.el): remove quotation marks in lean-execute

Browse source 
Close #294
This commit is contained in:
Soonho Kong 2014-11-05 09:20:14 -05:00
parent 5b87d060cf
commit e71db7109d
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) (defun lean-compile-string (exe-name args file-name)
"Concatenate exe-name, args, and 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) (defun lean-create-temp-in-system-tempdir (file-name prefix)
"Create a temp lean file and return its name" "Create a temp lean file and return its name"