Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#3682)
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 Aug 4, 2020
1 parent b215e95 commit acedda0
Showing 1 changed file with 0 additions and 6 deletions.
6 changes: 0 additions & 6 deletions scripts/nolints.txt
Expand Up @@ -1288,9 +1288,6 @@ apply_nolint unique doc_blame
-- measure_theory/category/Meas.lean
apply_nolint Meas doc_blame

-- measure_theory/integration.lean
apply_nolint measure_theory.measure.with_density doc_blame

-- measure_theory/measurable_space.lean
apply_nolint measurable_equiv has_inhabited_instance

Expand Down Expand Up @@ -1366,9 +1363,6 @@ apply_nolint fixed_points.next_fixed doc_blame
apply_nolint fixed_points.prev doc_blame
apply_nolint fixed_points.prev_fixed doc_blame

-- order/galois_connection.lean
apply_nolint galois_insertion has_inhabited_instance

-- order/lexicographic.lean
apply_nolint lex doc_blame

Expand Down

0 comments on commit acedda0

Please sign in to comment.