mathlib3
chore(gitignore): ignore files generated by mk_all script
#1328

Merged

chore(gitignore): ignore files generated by mk_all script #1328

mergify merged 2 commits into leanprover-community:master from robertylewis:ignore_all

chore(gitignore): ignore files generated by mk_all script

55ccb1bd

robertylewis requested a review 6 years ago

cipher1024 approved these changes on 2019-08-19

fpvandoorn added ready-to-merge

Merge branch 'master' into ignore_all

0f11d06d

mergify merged 733f616f into master 6 years ago

Reviewers

cipher1024

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone