vscode lean (opening new files on the left)

Stream: new members

[rzeta0]

This is a question abut vscode with the lean extension.

The view is split into two view, the left with the file contents for editing, and the right with the infoview.

Clicking on a new file sometimes / often opens it in the right pane in a new tab next to the info view. I have to manually drag the tab to the left pane.

All code files incl lean should ideally open on the left alongside the other tabs.

Anyone know why this happens and how to fix it? IIRC it didn't happen months ago.

[Rémy Degenne]

The files are opened in the view you selected last. So if your last action was to click something on the infoview that will happen. I also would like to open my files always on the left but I frequently open a file on the right by mistake because I clicked the "restart file" button, which is in that right view.