diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..23325f1 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,10 @@ +{ + "editor.insertSpaces": true, + "editor.tabSize": 2, + "editor.rulers" : [100], + "files.encoding": "utf8", + "files.eol": "\n", + "files.insertFinalNewline": true, + "files.trimFinalNewlines": true, + "files.trimTrailingWhitespace": true +} diff --git a/server/leanserver/.vscode/settings.json b/server/leanserver/.vscode/settings.json new file mode 100644 index 0000000..23325f1 --- /dev/null +++ b/server/leanserver/.vscode/settings.json @@ -0,0 +1,10 @@ +{ + "editor.insertSpaces": true, + "editor.tabSize": 2, + "editor.rulers" : [100], + "files.encoding": "utf8", + "files.eol": "\n", + "files.insertFinalNewline": true, + "files.trimFinalNewlines": true, + "files.trimTrailingWhitespace": true +}