chore(emacs/lean-info): fix a bug passing a wrong argument
This commit is contained in:
parent
fea516af24
commit
fc2fbc41bb
1 changed files with 1 additions and 1 deletions
|
@ -663,8 +663,8 @@ Take out \"BEGININFO\" and \"ENDINFO\" and Use \"ACK\" as a delim."
|
|||
"Return the full-name at point (if any)"
|
||||
(lean-get-info-record-at-point
|
||||
(lambda (info-record)
|
||||
(lean-server-debug "executing continuation for get-full-name-at-point")
|
||||
(funcall cont
|
||||
(lean-server-debug "executing continuation for get-full-name-at-point")
|
||||
(lean-get-full-name-at-point-cont info-record)))))
|
||||
|
||||
(provide 'lean-info)
|
||||
|
|
Loading…
Reference in a new issue