From 5d159ea664b40ada1a772404adcd338a2d96edca Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 28 Jul 2015 22:11:35 -0700 Subject: [PATCH] fix(emacs/lean-mode.el): fix wrong parens in lean-show-goal-at-pos --- src/emacs/lean-mode.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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)