Load not working after upgrading to v0.2.4

banacorn / agda-mode-vscode

agda-mode on VS Code

MIT License

169 stars 40 forks source link

Closed saulfield closed 3 years ago

saulfield commented 3 years ago

Hi, thank you for the great extension!

I am using Ubuntu 18.04 on WSL2. After upgrading to v0.2.4 I get an error when trying to load a file:

In settings.json I see that setting is already there, but it's greyed out and I see this on hover:

Everything works fine if I switch back to v0.2.3. It seems the setting is also greyed out and has that hover message in that version as well.

banacorn commented 3 years ago

Thanks!

I can reproduce this by clearing the agdaMode.agdaPath in the settings and then reload again.