chore(scripts): update nolints.txt (#10545)

I am happy to remove some nolints for you!
leanprover-community · Nov 30, 2021 · 396351b · 396351b
1 parent 04fc415
commit 396351b
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -366,7 +366,6 @@ apply_nolint stream.all doc_blame
 apply_nolint stream.any doc_blame
 apply_nolint stream.append_stream doc_blame
 apply_nolint stream.apply doc_blame
-apply_nolint stream.approx doc_blame
 apply_nolint stream.cons doc_blame
 apply_nolint stream.const doc_blame
 apply_nolint stream.corec doc_blame