Disable extra characters

Stream: new members

[Dan Piponi]

When using Lean in vscode, typing "(" results in "()" and typing "/-" results in "/--/". How do I stop this?

[Alex J. Best]

There is a vscode setting for this, pressing ctrl+, to open the settings, then search for Editor: auto-closing brackets and change it to never