mathlib3
chore(tactic/lint): typo
#2253
Merged

chore(tactic/lint): typo #2253

mergify merged 2 commits into master from time-class-typo
kim-em
kim-em chore(tactic/lint): typo
5148f2db
gebner
gebner approved these changes on 2020-03-27
gebner gebner added ready-to-merge
mergify[bot] Merge branch 'master' into time-class-typo
8d7dfd22
mergify mergify merged 451de279 into master 6 years ago
bryangingechen bryangingechen deleted the time-class-typo branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone