Update linter config

idris-lang · Sep 1, 2023 · f697ddd · f697ddd
1 parent a51da70
commit f697ddd
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/.github/linters/.chktexrc 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
@@ -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