mathlib3
doc(docs/install/project.md): mention that projects are git repositories
#2244
Merged

doc(docs/install/project.md): mention that projects are git repositories #2244

mergify merged 2 commits into master from doc-project-git
bryangingechen
bryangingechen doc(docs/install/project.md): mention that projects are git repositories
c595a3c8
kim-em
kim-em approved these changes on 2020-03-25
sgouezel sgouezel added ready-to-merge
mergify[bot] Merge branch 'master' into doc-project-git
84447128
mergify mergify merged 2fbf0070 into master 6 years ago
robertylewis robertylewis deleted the doc-project-git branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
Milestone