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

chore(emacs/lean-server): make lean-server-restart-all-processes interactive

Browse source
This commit is contained in:
Soonho Kong 2015-02-12 17:20:21 -05:00
parent 6bcd1a9980
commit a791953705
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -220,6 +220,7 @@
(defun lean-server-restart-all-processes ()
"Restart All lean-server processes"
;; (message "lean-server-restart-all-processes")
(interactive)
(lean-server-kill-process 'hott)
(lean-server-kill-process 'standard))