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

I am happy to remove some nolints for you!
leanprover-community · Feb 4, 2023 · c4bcf3a · c4bcf3a
1 parent ff6bde6
commit c4bcf3a
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 5 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -870,7 +870,4 @@ apply_nolint tactic.tidy.run_tactics doc_blame
 -- tactic/transfer.lean
 apply_nolint tactic.transfer doc_blame
 apply_nolint transfer.analyse_decls doc_blame
-apply_nolint transfer.compute_transfer doc_blame
-
--- tactic/wlog.lean
-apply_nolint tactic.wlog doc_blame
+apply_nolint transfer.compute_transfer doc_blame
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
@@ -73,4 +73,3 @@ src/tactic/tidy.lean : line 10 : ERR_MOD : Module docstring missing, or too late
 src/tactic/transfer.lean : line 6 : ERR_MOD : Module docstring missing, or too late
 src/tactic/transform_decl.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 src/tactic/trunc_cases.lean : line 9 : ERR_MOD : Module docstring missing, or too late
-src/tactic/wlog.lean : line 10 : ERR_MOD : Module docstring missing, or too late