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

fix(emacs/lean-mode.el): fix wrong parens in lean-show-goal-at-pos

Browse source
This commit is contained in:
Soonho Kong 2015-07-28 22:11:35 -07:00
parent 308af87b69
commit 5d159ea664
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/emacs/lean-mode.el
View file

@ -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)