mathlib3
feat(sanity_check): improve sanity_check
#1369
Merged

feat(sanity_check): improve sanity_check #1369

mergify merged 5 commits into master from sanity_improvements
fpvandoorn
fpvandoorn feat(sanity_check): improve sanity_check
5639459f
fpvandoorn typos
ca86ff9e
fpvandoorn fpvandoorn requested a review 6 years ago
fpvandoorn improve docstring
f5ed98af
fpvandoorn Also check for duplicated namespaces
028d49ae
cipher1024
cipher1024 commented on 2019-08-28
cipher1024 cipher1024 added ready-to-merge
cipher1024
cipher1024 approved these changes on 2019-08-30
mergify[bot] Merge branch 'master' into sanity_improvements
ae28bb8f
mergify mergify merged 2db7fa45 into master 6 years ago
mergify mergify deleted the sanity_improvements branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone