Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#3331)
Browse files Browse the repository at this point in the history
I am happy to remove some nolints for you!
  • Loading branch information
leanprover-community-bot committed Jul 9, 2020
1 parent 782013d commit 65dcf4d
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions scripts/nolints.txt
Expand Up @@ -1901,9 +1901,9 @@ apply_nolint tactic.interactive.mono_cfg doc_blame
apply_nolint tactic.interactive.mono_head_candidates doc_blame
apply_nolint tactic.interactive.mono_key doc_blame
apply_nolint tactic.interactive.mono_selection doc_blame
apply_nolint tactic.interactive.monotonicity.check doc_blame
apply_nolint tactic.interactive.monotonicity.check_rel doc_blame
apply_nolint tactic.interactive.monotonicity.attr doc_blame
apply_nolint tactic.interactive.monotonicity.check doc_blame
apply_nolint tactic.interactive.monotonicity.check_rel doc_blame
apply_nolint tactic.interactive.same_operator doc_blame
apply_nolint tactic.interactive.side doc_blame

Expand Down Expand Up @@ -1932,7 +1932,7 @@ apply_nolint tactic.interactive.fold_assoc doc_blame
apply_nolint tactic.interactive.fold_assoc1 doc_blame
apply_nolint tactic.interactive.hide_meta_vars' doc_blame
apply_nolint tactic.interactive.list.minimum_on doc_blame
apply_nolint tactic.interactive.match_ac doc_blame unused_arguments
apply_nolint tactic.interactive.match_ac doc_blame
apply_nolint tactic.interactive.match_ac' doc_blame
apply_nolint tactic.interactive.match_chaining_rules doc_blame
apply_nolint tactic.interactive.match_prefix doc_blame
Expand All @@ -1942,7 +1942,7 @@ apply_nolint tactic.interactive.mk_congr_law doc_blame
apply_nolint tactic.interactive.mk_fun_app doc_blame
apply_nolint tactic.interactive.mk_pattern doc_blame
apply_nolint tactic.interactive.mk_rel doc_blame
apply_nolint tactic.interactive.mono_aux doc_blame unused_arguments
apply_nolint tactic.interactive.mono_aux doc_blame
apply_nolint tactic.interactive.mono_function doc_blame
apply_nolint tactic.interactive.mono_function.to_tactic_format doc_blame
apply_nolint tactic.interactive.mono_law doc_blame
Expand Down Expand Up @@ -2319,4 +2319,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

0 comments on commit 65dcf4d

Please sign in to comment.