mathlib3
feat(lint): avoid Travis error when declarations are renamed
#1771

Merged

feat(lint): avoid Travis error when declarations are renamed #1771

mergify merged 2 commits into master from travis_lint

feat(lint): avoid Travis error when declarations are renamed

8d090800

fpvandoorn approved these changes on 2019-12-03

fpvandoorn added ready-to-merge

Merge branch 'master' into travis_lint

40cc592b

mergify merged 827e78b1 into master 6 years ago

mergify deleted the travis_lint branch 6 years ago

Reviewers

fpvandoorn

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone