vscode-idris icon indicating copy to clipboard operation
vscode-idris copied to clipboard

Published 20 hours ago • verified publisher icon zjhmale

Preserve focus when showing output channel

Open jasper-d opened this issue 5 years ago • 2 comments

This fixes #124 by passing true for the optional preserveFocus parameter when invoking show on the outputChannel. See https://code.visualstudio.com/docs/extensionAPI/vscode-api#OutputChannel.show for documentation.

jasper-d avatar Oct 08 '18 21:10 jasper-d

Closing and reopening PR to re-trigger Travis CI build

jasper-d avatar Oct 09 '18 16:10 jasper-d

Could this please be merged!

timjs avatar May 04 '20 16:05 timjs