index.md): remove obsolete recommendation to use lean-3.7.2 branch
#2206

Merged

doc(docs/contribute/index.md): remove obsolete recommendation to use lean-3.7.2 branch #2206

mergify merged 1 commit into master from remove-obsolete-doc

doc(docs/contribute/index.md): remove obsolete recommendation to use …

3c4e38fa

PatrickMassot added ready-to-merge

PatrickMassot approved these changes on 2020-03-21

mergify merged dd85db0c into master 6 years ago

mergify deleted the remove-obsolete-doc branch 6 years ago

Reviewers

PatrickMassot

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone