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

Published 20 hours ago • verified publisher icon zjhmale

Output channel is focused

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

Summary: Whenever the output channel is shown it takes the focus (i.e. becomes the active editor window), making it impossible to write more a few characters.

Repro: Open an .idr file and make a minor edit (e.g. add a comment)

Expected: Nothing in particular

Actual: Output becomes the active window (the cursor moves to the Output window)

Environment:

  • Visual Studio Code 1.28.0, Git hash 431ef9da3cf88a7e164f9d33bf62695e07c6c2a9, Architecture: ia32
  • vscode-idris: v.0.9.8
  • OS: Win 10 x64

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

Super annoying issue!

coffius avatar Apr 27 '19 14:04 coffius

Any progress on this?

timjs avatar May 04 '20 16:05 timjs