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

fix(emacs/lean-mode.el): use original extension when make temp-file

Browse source 
close #767
This commit is contained in:
Soonho Kong 2015-08-05 12:51:09 -04:00
parent fc6b41ee0e
commit 7d1895928a
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

@ -37,7 +37,7 @@
(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"
(make-temp-file (or prefix "flymake") nil ".lean")) (make-temp-file (or prefix "flymake") nil (f-ext file-name)))
(defun lean-execute (&optional arg) (defun lean-execute (&optional arg)
"Execute Lean in the current buffer" "Execute Lean in the current buffer"