From 76234167723824f6d7c36b2a7be51e9d190bdf03 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 20 Oct 2022 11:58:25 +0200
Subject: [PATCH] add vs code settings

---
 .vscode/settings.json                   | 10 ++++++++++
 server/leanserver/.vscode/settings.json | 10 ++++++++++
 2 files changed, 20 insertions(+)
 create mode 100644 .vscode/settings.json
 create mode 100644 server/leanserver/.vscode/settings.json

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
+}