Merge branch 'main' into incompatible-visibilities

idris-lang · Oct 24, 2023 · 3e7d5aa · 3e7d5aa
2 parents e9b66a1 + 46be3b8
commit 3e7d5aa
Show file tree

Hide file tree

Showing 3,084 changed files with 5,367 additions and 5,184 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