mathlib3
chore(travis): add instance priority linter to CI
#1787

Merged

chore(travis): add instance priority linter to CI #1787

mergify merged 3 commits into master from robertylewis-patch-1

add instance priority to linter

38ac7bcc

Update mk_nolint.lean

17af0572

fix fintype.compact_space prio

87c1913d

sgouezel added ready-to-merge

sgouezel approved these changes on 2019-12-06

mergify merged 6968d749 into master 6 years ago

mergify deleted the robertylewis-patch-1 branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone