feat(emacs/lean-mode.el): use --dir
option in lean-exec-at-pos
See #821 and #788
This commit is contained in:
parent
f78e57fd52
commit
b4b365239f
1 changed files with 2 additions and 0 deletions
|
@ -154,6 +154,8 @@ will be flushed everytime it's executed."
|
|||
,process-buffer-name
|
||||
,(lean-get-executable lean-executable-name)
|
||||
,lean-mode-option
|
||||
"--dir"
|
||||
,(f-dirname (buffer-file-name))
|
||||
"--line"
|
||||
,(int-to-string (line-number-at-pos))
|
||||
"--col"
|
||||
|
|
Loading…
Reference in a new issue