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

fix(emacs/lean-server.el): invoke lean --server from project root if existent

Browse source
This commit is contained in:
Sebastian Ullrich 2016-04-08 23:38:45 +02:00 committed by Leonardo de Moura
parent 08c55754a9
commit 5810a4de8f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,6 +12,7 @@
(require 'lean-variable)
(require 'lean-cmd)
(require 'lean-info)
(require 'lean-project)
(require 'lean-util)
;; Parameters
@ -175,6 +176,7 @@
;; (message "lean-server-create-process")
(let* ((type (or type (lean-choose-minor-mode-based-on-extension)))
(process-connection-type nil)
(default-directory (or (lean-project-find-root) default-directory))
(p (apply 'start-process
(append (list (lean-server-process-name type)
(lean-server-buffer-name type)