search

meraymond2 / idris-vscode

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

Support v0.4.0 #57

Closed meraymond2 closed 3 years ago

meraymond2 commented 3 years ago

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

meraymond2 commented 3 years ago

https://github.com/meraymond2/idris-vscode/pull/59

meraymond2 commented 3 years ago

It doesn't look like the :search command is implemented for the IDE mode, so I don't know that there's anything more to do.