Go to definition opening in infoview tab

Stream: general

[Bolton Bailey]

The behavior of VSCode has changed recently for me: When I "Go to definition" with a side panel open for InfoView, it opens the new file in the side panel. I don't want this because I have to manually move it back over - it used to just open in the same panel as the file I was clicking from. Does anyone know why this change happened and how I can get the old behavior back?

[Mario Carneiro]

see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/InfoView.20focus.20issue