Add .editorconfig

monsterkrampe · Aug 25, 2024 · ed67167 · ed67167
1 parent 0930b2d
commit ed67167
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/.editorconfig b/.editorconfig
@@ -0,0 +1,10 @@
+root = true
+
+[*]
+end_of_line = lf
+insert_final_newline = true
+
+[*.lean]
+indent_style = space
+indent_size = 2
+