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

fix(emacs/lean-server): disable undo and hide process buffers

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-06 19:48:29 +01:00 • committed by Leonardo de Moura
parent 5e3f26ec95
commit 7770e87f69
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -93,7 +93,7 @@
(proc (if (fboundp 'make-process)
(make-process ;; emacs >= 25 lets us redirect stderr
:name "lean-server"
:buffer (format "*lean-server (%s)*" project-dir)
:buffer (format " *lean-server (%s)*" project-dir)
:command `(,(lean-get-executable lean-executable-name)
"--server"
,(format "*%s*" project-dir))
@ -105,7 +105,7 @@
:buffer (format "*lean-server stderr (%s)*" project-dir)
:noquery t))
(start-file-process "lean-server"
(format "*lean-server (%s)*" (buffer-name))
(format " *lean-server (%s)*" (buffer-name))
(lean-get-executable lean-executable-name)
"--server"
(format "*%s*" (buffer-name)))))