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

I am happy to remove some nolints for you!
leanprover-community · Aug 7, 2020 · 49ba4c4 · 49ba4c4
1 parent 1930601
commit 49ba4c4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -2156,4 +2156,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame