parent
37e514e114
commit
3b574ef31d
1 changed files with 6 additions and 0 deletions
|
@ -395,4 +395,10 @@ If it's successful, take it out from the queue. Otherwise, set an
|
|||
(when lean-global-async-task-queue
|
||||
(lean-server-set-timer-for-event-handler)))
|
||||
|
||||
(defadvice save-buffers-kill-emacs
|
||||
(before lean-server-kill-before-kill-emacs activate)
|
||||
"Call `lean-server-kill-process', to avoid the user being
|
||||
prompted to kill the lean-server process."
|
||||
(lean-server-kill-process))
|
||||
|
||||
(provide 'lean-server)
|
||||
|
|
Loading…
Reference in a new issue