Workspace json

Stream: general

[Filippo A. E. Nuccio]

I see that two weeks ago @Kim Morrison added the line

"editor.acceptSuggestionOnEnter": "off",

to the json file, but this can be painful for users (like me...) who are happy to hit Enter to accept suggestions. The problem is that workspace settings always overwrite users one, and I wonder why this should really be part of Mathlib.

[Julian Berman]

c.f. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/propose.20removing.20module.20docstring.20code.20suggestion/near/439229009

[Filippo A. E. Nuccio]

Well, I really cannot see why we should decide as a community how people want to use their VSCode...

[Shreyas Srinivas]

Agreed. This is super intrusive and overrides user settings.

[Julian Berman]

(I agree :) but I think you should probably both say so in that thread)

[Filippo A. E. Nuccio]

I tried, and if you both agree please help me :smile:

[Shreyas Srinivas]

I am not sure my opinion will even remotely outweigh an already merged PR, but I can help

[Kim Morrison]

Sorry, when I did this I thought I was setting a better default for new users, but did not realise that workspace settings would override user settings, and so experts (or generally, people who thought they knew better!) can't override it. :-(