chore(scripts): update nolints.json (#19137)

I am happy to remove some nolints for you!
leanprover-community · Nov 17, 2024 · fe4de19 · fe4de19
1 parent 08fa0e9
commit fe4de19
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/scripts/nolints.json b/scripts/nolints.json
@@ -149,9 +149,6 @@
  ["docBlame", "FirstOrder.«term∀'_»"],
  ["docBlame", "FirstOrder.«term∃'_»"],
  ["docBlame", "FirstOrder.«term∼_»"],
- ["docBlame", "Function.app"],
- ["docBlame", "Function.compLeft"],
- ["docBlame", "Function.compRight"],
  ["docBlame", "Function.swap"],
  ["docBlame", "Function.«term_∘'_»"],
  ["docBlame", "HSpace.e"],