mathlib3
refactor(data/rat/meta): rename to meta_defs
#1612
Merged

refactor(data/rat/meta): rename to meta_defs #1612

mergify merged 2 commits into master from rename_rat_meta
robertylewis
robertylewis refactor(data/rat/meta): rename to meta_defs
c6f61ecb
rwbarton
rwbarton approved these changes on 2019-10-25
rwbarton rwbarton added ready-to-merge
bryangingechen fix build
a9ba63d0
mergify mergify merged 6ee8bf97 into master 6 years ago
mergify mergify deleted the rename_rat_meta branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone