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

I am happy to remove some nolints for you!
leanprover-community · Sep 18, 2020 · 52d4b92 · 52d4b92
1 parent 5a2e7d7
commit 52d4b92
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -939,6 +939,9 @@ apply_nolint gaussian_int doc_blame
 apply_nolint gaussian_int.div doc_blame
 apply_nolint gaussian_int.mod doc_blame
 
+-- deprecated/subfield.lean
+apply_nolint is_subfield doc_blame
+
 -- deprecated/subgroup.lean
 apply_nolint add_group.closure doc_blame
 apply_nolint add_group.in_closure doc_blame
@@ -968,9 +971,6 @@ apply_nolint mv_polynomial.indicator doc_blame
 apply_nolint mv_polynomial.restrict_degree doc_blame
 apply_nolint mv_polynomial.restrict_total_degree doc_blame
 
--- field_theory/subfield.lean
-apply_nolint is_subfield doc_blame
-
 -- group_theory/abelianization.lean
 apply_nolint abelianization.lift doc_blame