From 75d87f34a6388bf3c24fa53887b031699c99e068 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 Mar 2021 10:45:04 +0100 Subject: [PATCH] chore: lean4-mode: do not re-request goal on each flycheck change --- lean4-mode/lean4-mode.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean4-mode/lean4-mode.el b/lean4-mode/lean4-mode.el index 329a212ac1..44b3fa1eea 100644 --- a/lean4-mode/lean4-mode.el +++ b/lean4-mode/lean4-mode.el @@ -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.