You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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:
The text was updated successfully, but these errors were encountered: