Closed mhuisi closed 3 weeks ago
This PR allows the Infoview to be detached into a separate window (e.g. for use on a second monitor).
Issue originally reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VSCode.20floating.20infoview/near/437975918.
This PR allows the Infoview to be detached into a separate window (e.g. for use on a second monitor).
Issue originally reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VSCode.20floating.20infoview/near/437975918.