From f697ddd929025d7ec49fedf80a94eeaf7cd6ed18 Mon Sep 17 00:00:00 2001
From: Robert Wright <robert.wright@ed.ac.uk>
Date: Fri, 1 Sep 2023 14:37:24 +0100
Subject: [PATCH] Update linter config

---
 .github/linters/.chktexrc          | 14 ++++++++++++++
 .github/linters/.markdown-lint.yml |  1 +
 2 files changed, 15 insertions(+)
 create mode 100644 .github/linters/.chktexrc

diff --git a/.github/linters/.chktexrc b/.github/linters/.chktexrc
new file mode 100644
index 00000000000..3b3a676c60d
--- /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 8f250e870c7..b1f878d305c 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