Skip to content

Issues: zjhmale/vscode-idris

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort

Issues list

Support idris2
#132 opened Oct 4, 2020 by turion
Cannot run extension on Windows
#128 opened Feb 26, 2020 by Pzixel
Output channel is focused
#124 opened Oct 8, 2018 by jasper-d
make-lemma seem don't work
#123 opened Jun 7, 2018 by jiamo
Default Keyboard Shortcuts
#120 opened Mar 4, 2018 by namuol
Icon & Website working in progress
#78 opened Apr 15, 2017 by zjhmale
2 tasks
Support formatter discussion
#77 opened Apr 14, 2017 by zjhmale
More sophisticated test cases
#47 opened Mar 29, 2017 by zjhmale
Completion improvement
#31 opened Mar 26, 2017 by zjhmale
1 of 2 tasks
Support more commands
#30 opened Mar 26, 2017 by zjhmale
3 of 10 tasks
ProTip! Exclude everything labeled bug with -label:bug.