mathlib3
feat(scripts): add scripts to import all mathlib files
#1281

Merged

feat(scripts): add scripts to import all mathlib files #1281

mergify merged 5 commits into master from mk_all

add scripts to import all mathlib files

3e79015f

fpvandoorn requested a review 7 years ago

jcommelin commented on 2019-07-30

also delete all.olean files

98cad179

remove unnecessary maxdepth

802ada0e

add comments, and generate comments

4a5a51d9

robertylewis changed the title ~~add scripts to import all mathlib files~~ feat(scripts): add scripts to import all mathlib files 7 years ago

robertylewis approved these changes on 2019-08-12

robertylewis added ready-to-merge

Merge branch 'master' into mk_all

01e7d255

mergify merged 900c53ae into master 7 years ago

mergify deleted the mk_all branch 7 years ago

Reviewers

robertylewis

jcommelin

khoek

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone