diff --git a/.github/linters/.chktexrc b/.github/linters/.chktexrc new file mode 100644 index 000000000..3b3a676c6 --- /dev/null +++ b/.github/linters/.chktexrc @@ -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 +} diff --git a/.github/linters/.markdown-lint.yml b/.github/linters/.markdown-lint.yml index 8f250e870..b1f878d30 100644 --- a/.github/linters/.markdown-lint.yml +++ b/.github/linters/.markdown-lint.yml @@ -32,6 +32,7 @@ MD026: MD029: false # Ordered list item prefix MD033: false # Allow inline HTML 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 code_blocks: false html_elements: false