Idris2/.editorconfig

[*.idr]
end_of_line = lf
insert_final_newline = true
charset = utf-8
indent_style = space
indent_size = 2
trim_trailing_whitespace = true
Add .editorconfig Add .editorconfig to the repository to trim trailing whitespaces and insert trailing newlines in many editors. See also #931 2021-01-16 10:35:59 +03:00			`[*.idr]`
			`end_of_line = lf`
			`insert_final_newline = true`
			`charset = utf-8`
			`indent_style = space`
Specify tab size in .editorconfig ... as 2. 2021-01-21 02:36:01 +03:00			`indent_size = 2`
Add .editorconfig Add .editorconfig to the repository to trim trailing whitespaces and insert trailing newlines in many editors. See also #931 2021-01-16 10:35:59 +03:00			`trim_trailing_whitespace = true`