fix(emacs/lean-type): lean-helm-definitions: disable client-side filtering & caching
This commit is contained in:
parent
ac0be0ecc6
commit
cfbb298a2a
1 changed files with 2 additions and 0 deletions
|
|
@ -165,6 +165,8 @@
|
|||
(helm :sources (helm-build-sync-source "helm-source-lean-definitions"
|
||||
:requires-pattern t
|
||||
:candidates 'lean-helm-definitions-candidates
|
||||
:volatile t
|
||||
:match 'identity
|
||||
:action '(("Go to" . (lambda (c) (with-helm-current-buffer
|
||||
(apply 'lean-find-definition-cont (plist-get c :source)))))))
|
||||
:buffer "*helm Lean definitions*"))
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue