diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json index 9261ebb6..d7c84cd3 100644 --- a/vscode-lean4/package.json +++ b/vscode-lean4/package.json @@ -1754,7 +1754,10 @@ "files.insertFinalNewline": true, "files.trimFinalNewlines": true, "files.trimTrailingWhitespace": true, - "editor.quickSuggestionsDelay": 200 + "editor.quickSuggestionsDelay": 200, + "editor.formatOnSave": false, + "editor.formatOnPaste": false, + "editor.formatOnType": false } }, "walkthroughs": [