Implement workbench.editor.revealIfOpen preference#12145

Merged

colin-grant-work merged 1 commit intoeclipse-theia:masterfrom colin-grant-work:feature/workbench-reveal-preference

Feb 6, 2023

+17-10

Commits on Feb 3, 2023

Implement workbench.editor.revealIfOpen preference
colin-grant-work
committed