search

leanprover / lean3-mode

Emacs mode for Lean
Apache License 2.0
69 stars 17 forks source link

Don't Display Current Flycheck Message in Minibuffer when *Flycheck Errors* Buffer is Visible #14

Open odanoburu opened 5 years ago

odanoburu commented 5 years ago

mirroring https://github.com/flycheck/flycheck/issues/302

when using vanilla flycheck, doing

(setq flycheck-display-errors-function #'flycheck-display-error-messages-unless-error-list)

solves this issue. however from my understanding of the code lean-mode is handling error display manually, and the fix is not so simple (although it might still be pretty simple).