I expected the infoview to close automatically when I :q a Lean file with an infoview open to its side. Particularly when this Lean file is the only file open and I would like that to cause to quit Neovim entirely.
Does this make sense as an option or even as default behavior?
This is definitely reasonable to expect yeah, this is tracked in #43. Going to close this but feel free to stick thoughts there. Maybe I'll carve out some time to finally knock it off.
I expected the infoview to close automatically when I
:q
a Lean file with an infoview open to its side. Particularly when this Lean file is the only file open and I would like that to cause to quit Neovim entirely.Does this make sense as an option or even as default behavior?