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

fix(emacs/lean-server): use lean-get-executable

Browse source
This commit is contained in:
Sebastian Ullrich 2016-10-13 12:22:50 -04:00 • committed by Leonardo de Moura
parent fd467584bd
commit 3eb007166d
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -37,7 +37,9 @@
(process-connection-type nil))
(start-file-process "lean-server"
(format "*lean-server (%s)*" (buffer-name))
"lean" "--server" (format "*%s*" (buffer-name)))))
(lean-get-executable lean-executable-name)
"--server"
(format "*%s*" (buffer-name)))))
(set-process-query-on-exit-flag lean-server-process nil)
(setq lean-server-handler-tq (tq-create lean-server-process))))