search

leanprover / lean3-mode

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

Prevent lean-server from complaining when disabling flycheck #42

Open kozytskyiad opened 2 years ago

kozytskyiad commented 2 years ago

I searched the functions provided by the mode and lean-toggle-flycheck-mode appears to be the intended way to disable flycheck, but whenever I toggle it (either manually or via hook) lean-mode complains about it:

error in lean-server command handler: (user-error Flycheck mode disabled)
Server response was:

What is the proper way to disable flycheck with lean-mode then?