mathlib3
doc(contribute/index.md): add line about large PRs [ci skip]
#1267

Merged

doc(contribute/index.md): add line about large PRs [ci skip] #1267

robertylewis merged 2 commits into master from robertylewis-patch-1

doc(contribute/index.md): add line about large PRs [ci skip]

0e3e4f92

robertylewis requested a review 6 years ago

PatrickMassot added ready-to-merge

PatrickMassot approved these changes on 2019-07-25

Merge branch 'master' into robertylewis-patch-1

d41d7447

robertylewis merged d5a53939 into master 6 years ago

robertylewis deleted the robertylewis-patch-1 branch 6 years ago

Reviewers

PatrickMassot

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone