Configurably autoclose the infoview if it has no Lean buffers updating it
Open
enhancement
infoview
- Dominant language
- Lua
- Stars
- 581
- Forks
- 60
- Avg merge
- 4d 12h
- Merged PRs (30d)
- 2
Description
Add a configuration option `infoview.autoclose = true (default)` which indicates the infoview should be closed if no Lean buffers are updating it anymore (e.g. particularly if it is the last remaining window).
Contributor guide
Assessment
This issue has not been assessed yet.