diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index cf9f3853b1..e49b5aaa5b 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -234,6 +234,7 @@ placeholder, call lean-server with --hole option, otherwise call
   (local-set-key lean-keybinding-show-key                  'quail-show-key)
   (local-set-key lean-keybinding-set-option                'lean-set-option)
   (local-set-key lean-keybinding-eval-cmd                  'lean-eval-cmd)
+  (local-set-key lean-keybinding-server-restart            'lean-server-restart)
   (local-set-key lean-keybinding-tab-indent-or-complete    'lean-tab-indent-or-complete)
   (local-set-key lean-keybinding-lean-show-goal-at-pos     'lean-show-goal-at-pos)
   (local-set-key lean-keybinding-lean-show-id-keyword-info 'lean-show-id-keyword-info)
@@ -263,6 +264,7 @@ placeholder, call lean-server with --hole option, otherwise call
     ["List of errors"       flycheck-list-errors              (and lean-flycheck-use flycheck-mode)]
     "-----------------"
     ["Clear all cache"      lean-clear-cache                  t]
+    ["Restart lean process" lean-server-restart               t]
     "-----------------"
     ("Configuration"
      ["Use flycheck (on-the-fly syntax check)"
diff --git a/src/emacs/lean-server.el b/src/emacs/lean-server.el
index 221bf6f7dc..c55cc3a560 100644
--- a/src/emacs/lean-server.el
+++ b/src/emacs/lean-server.el
@@ -49,7 +49,9 @@
   (interactive)
   (lean-server-stop)
   (lean-server-start)
-  (when lean-flycheck-use (flycheck-buffer)))
+  (when lean-flycheck-use
+    (flycheck-stop)
+    (flycheck-buffer)))
 
 (defun lean-server-send-command-handler (closure answer)
   "Callback for lean-server-send-command"
diff --git a/src/emacs/lean-settings.el b/src/emacs/lean-settings.el
index 1d7f9371dc..212158a4a8 100644
--- a/src/emacs/lean-settings.el
+++ b/src/emacs/lean-settings.el
@@ -157,6 +157,9 @@ false (nil)."
 (defcustom lean-keybinding-eval-cmd (kbd "C-c C-e")
   "Lean Keybinding for eval-cmd"
   :group 'lean-keybinding  :type 'key-sequence)
+(defcustom lean-keybinding-server-restart (kbd "C-c C-r")
+  "Lean Keybinding for server-restart"
+  :group 'lean-keybinding  :type 'key-sequence)
 (defcustom lean-keybinding-tab-indent-or-complete (kbd "TAB")
   "Lean Keybinding for tab-indent-or-complete"
   :group 'lean-keybinding  :type 'key-sequence)