search

meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
59 stars 10 forks source link

Version 0.5.0 #65

Closed meraymond2 closed 3 years ago

meraymond2 commented 3 years ago

https://github.com/idris-lang/Idris2/blob/ada3eb44498b53bf3e4673709ac7fab893da1d75/CHANGELOG.md

It doesn't look like there are any relevant changes to the IDE mode, but I want to check that all the tests are still passing, and at the very least will update the readme.

meraymond2 commented 3 years ago

I think the only relevant thing is that the List Metavariables command was broken, but it's been subsequently fixed. If you're building from the main branch, it'll be fine, but with the 0.5.0 release, the command won't do anything do to a JS exception.

Since it doesn’t break the whole plugin, just that one command, I'm inclined to just wait for it to be fixed in the next release, rather than implement a workaround specifically for 0.5.0, because that would break it for anyone using a previous or later version.