Open jp-diegidio opened 8 months ago
Thanks for the bug report @jp-diegidio , a few comments:
coq-lsp.updateIgnores
settingon
, now after more feedback, it seems that there is some split about what the default should be, but indeed I propose we turn this setting off
for the 0.2.x series, which is due soon. I do agree that the least intrusive behavior is better.There is still a usability problem here, in terms of discoverability. IMHO we should proceed as follows:
Hi @ejgallego, thank you.
IMO, this is really a misfeature (I am talking requirements engineering and what that would have to say), but never mind, as long as it is controllable.
As for usability/discoverability, VSCode/ium ships with a Settings editor already: all I'd really want (suggest) is to have all Settings actually and fully documented wherever they must be (the rest would be additional/auxiliary and again possibly spurious features that could/should be avoided IMO, anyway this is beside the point).
Describe the bug
Upon activation, the plugin adds entries to the ".vscode/settings.json" file, which represents Workspace Settings, or creates the file if it does not exist already.
Specifically, the following entries are prepended to (and removed from) any pre-existing entries within the "files.exclude" object:
To Reproduce
Assuming the plugin is installed and enabled, just activate it in any way, from opening a ".v" file to opening the Goals window.
Expected behavior
The plugin should not touch the Settings file.
Ad interim (?), there should at least be a flag configurable in Settings to enable/disable this behaviour, and false by default.
Desktop (please complete the following information):