max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lean4-mode: do not re-request goal on each flycheck change

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-11 10:45:04 +01:00
parent f4ed9686aa
commit 75d87f34a6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean4-mode/lean4-mode.el
View file

@ -153,7 +153,7 @@
(before-save-hook . lean4-whitespace-cleanup)
;; info windows
(post-command-hook . lean4-info-buffer-refresh)
(flycheck-after-syntax-check-hook . lean4-info-buffer-refresh)
(flycheck-after-syntax-check-hook . lean4-info-buffer-redisplay)
)
"Hooks which lean4-mode needs to hook in.