Remove annoying warning for hover

[zjhmale]

https://github.com/zjhmale/vscode-idris/blob/master/src/idris/commands.js#L41

[philipcraig]

This message is indeed quite annoying. How can I install a pre-release, if the release is going to be a few days?

[zjhmale]

@philipcraig, sorry for that, I will release it now 😅

[zjhmale]

Hi @philipcraig, v0.3.7 is already released.

[philipcraig]

Thanks for the release! However, all I now get on all hovers is a message saying "didn't load path/to/source.idr" where the path is my path. Even hello world does this.

Edited: please disregard. I had accidentally done a stack install of a very old Idris version.

[zjhmale]

@philipcraig That is because the Idris file itself can not be type checked, maybe I should show the error message directly instead of showing this confusing message.

[philipcraig]

Good idea to show Idris's messages directly. If I'd been able to see Idris' message, which was about incompatible versions and advised cleaning the .ibc files, I'd have known what to do.

[zjhmale]

Yes, we need to create an issue here, maybe you can do me the favor 😄 Thanks!

[philipcraig]

will do