Idris2/.github/linters/.ecrc

{
  "Exclude" : ["expected"],
  "Disable": {
    "IndentSize": true,
    "Indentation": true
  }
}
Add super-linter Example run with error: [here](https://github.com/stepancheg/Idris2/runs/1718861440?check_suite_focus=true) The downside is super-linter runs for 3 minutes. But that's probably expected since the linter is [provided by GitHub](https://github.com/github/super-linter). Two days ago when I submitted #931 I did not know super-linter exists. 2021-01-18 05:28:51 +03:00			`{`
Exclude "expected" files from linting Those files are part of tests and hold what should be the output of the compiler. If they are included in the linting, warnings will be emitted when one of the tests in which the compiler outputs a line with trailing whitespace is edited, which is not desirable. 2021-01-29 20:53:14 +03:00			`"Exclude" : ["expected"],`
Add super-linter Example run with error: [here](https://github.com/stepancheg/Idris2/runs/1718861440?check_suite_focus=true) The downside is super-linter runs for 3 minutes. But that's probably expected since the linter is [provided by GitHub](https://github.com/github/super-linter). Two days ago when I submitted #931 I did not know super-linter exists. 2021-01-18 05:28:51 +03:00			`"Disable": {`
			`"IndentSize": true,`
Disable indents check (properly this time) * `.ecrc` was in incorrect directory * add another option for extra precaution 2021-01-21 17:13:35 +03:00			`"Indentation": true`
Add super-linter Example run with error: [here](https://github.com/stepancheg/Idris2/runs/1718861440?check_suite_focus=true) The downside is super-linter runs for 3 minutes. But that's probably expected since the linter is [provided by GitHub](https://github.com/github/super-linter). Two days ago when I submitted #931 I did not know super-linter exists. 2021-01-18 05:28:51 +03:00			`}`
			`}`