mathlib3
fix(naming): typo [ci skip]
#1401
Merged

fix(naming): typo [ci skip] #1401

mergify merged 3 commits into master from naming_typo
fpvandoorn
fpvandoorn fix(naming): typo [ci skip]
a2da5ce1
fpvandoorn fpvandoorn requested a review 6 years ago
digama0
digama0 commented on 2019-09-05
fpvandoorn more typos
615179c0
digama0
digama0 approved these changes on 2019-09-05
fpvandoorn fpvandoorn added ready-to-merge
mergify[bot] Merge branch 'master' into naming_typo
cba1e468
mergify mergify merged 1a0ed809 into master 6 years ago
mergify mergify deleted the naming_typo branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone