mathlib3
doc(contribute/style): remove outdated syntax [ci skip]
#1329

Merged

doc(contribute/style): remove outdated syntax [ci skip] #1329

mergify merged 3 commits into master from style

doc(contribute/style): remove outdated syntax [ci skip]

0f24970f

robertylewis requested a review 7 years ago

doc(contribute/style): mistaken find/replace

b74444ab

ChrisHughes24 added ready-to-merge

ChrisHughes24 approved these changes on 2019-08-15

Merge branch 'master' into style

181640c0

mergify merged ebbbb76b into master 7 years ago

mergify deleted the style branch 7 years ago

Reviewers

ChrisHughes24

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone