Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Don't emit any user-facing messages via vim.notify.
For users not using nvim-notify (for whatever reason), the log level isn't respected in the sense that no filtering is done by default, so even debug messages will *synchronously* interrupt users from typing or moving around Lean files.
- Loading branch information