project.md): mention that projects are git repositories (#2244)

Commit

6 years ago

doc(docs/install/project.md): mention that projects are git repositories (#2244) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

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

Author

bryangingechen

Parents

75b4ee86

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

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