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

I am happy to remove some nolints for you!
leanprover-community · May 14, 2020 · 03c272e · 03c272e
1 parent 2871bd1
commit 03c272e
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1792,9 +1792,7 @@ apply_nolint function.embedding.subtype_map doc_blame
 apply_nolint function.embedding.sum_congr doc_blame
 apply_nolint function.embedding.trans doc_blame
 
--- logic/function.lean
-apply_nolint function.bicompl doc_blame
-apply_nolint function.bicompr doc_blame
+-- logic/function/basic.lean
 apply_nolint function.uncurry' doc_blame
 
 -- logic/relation.lean