-
Notifications
You must be signed in to change notification settings - Fork 21
Open
Description
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
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels