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

remove "machine-overridable" scope from some settings #109

Closed kzvi closed 2 years ago

kzvi commented 2 years ago

These settings are user interface settings and should probably not be marked "machine-overridable", so that they can be synced. This makes this extension more consistent with other extensions.

banacorn commented 2 years ago

Thank you!