diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 865f1b6ca..90ea8f2bd 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -157,10 +157,10 @@ placeholder, call lean-server with --hole option, otherwise call (or (char-equal cb ?\s) (char-equal cb ?\t) (char-equal cb ?\n) - (char-equal cb ?\r)))) + (char-equal cb ?\r))))) (lean-exec-at-pos "lean-hole" "*Lean Goal*" "--hole")) (t - (lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal"))))) + (lean-exec-at-pos "lean-goal" "*Lean Goal*" "--goal")))) (defun lean-std-exe () (interactive)