search

banacorn / agda-mode-vscode

agda-mode on VS Code
https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode
MIT License
169 stars 39 forks source link

Don't store the agda path in the config #112

Closed ncfavier closed 2 years ago

ncfavier commented 2 years ago

When switching between projects that use different versions of Agda, I have to clear the agda path and restart vscode every time, which is annoying.

If there is a use case for saving the path in the config, we could expose this as a setting. Or maybe only save when the path is not empty.

I couldn't build rescript on NixOS so I didn't regenerate the javascript.

ncfavier commented 2 years ago

My current workaround for this is to set the Agda path to a shell script that just does exec agda "$@".

banacorn commented 2 years ago

Thanks!

ncfavier commented 2 years ago

Don't forget to rebuild the JS!