idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

Update linter config

Browse Source
This commit is contained in:
Robert Wright 2023-09-01 14:37:24 +01:00 committed by G. Allais
parent 424bc20c27
commit cf73efe8e0
2 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
.github/linters/.chktexrc vendored Normal file
View File

@ -0,0 +1,14 @@
########################
########################
## LaTeX Linter rules ##
########################
########################
CmdLine {
# Command terminated with space.
--nowarn 1
# You ought to remove spaces in front of punctuation.
# This gets confused in code blocks, failing on eg. `x : Nat`
--nowarn 26
}

1
.github/linters/.markdown-lint.yml vendored
View File

@ -32,6 +32,7 @@ MD026:
MD029: false # Ordered list item prefix MD029: false # Ordered list item prefix
MD033: false # Allow inline HTML MD033: false # Allow inline HTML
MD036: false # Emphasis used instead of a heading MD036: false # Emphasis used instead of a heading
MD041: false # First line in file should be a top level heading
MD044: # Proper names should have the correct capitalization MD044: # Proper names should have the correct capitalization
code_blocks: false code_blocks: false
html_elements: false html_elements: false