mathlib3
doc(contribute/style.md): fix section on comments [ci skip]
#1265

Merged

doc(contribute/style.md): fix section on comments [ci skip] #1265

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

doc(contribute/style.md): fix section on comments [ci skip]

fb023fa9

robertylewis requested a review 6 years ago

Merge branch 'master' into robertylewis-patch-1

d796de11

robertylewis merged 926467dc into master 6 years ago

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

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Milestone

No milestone