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

Commit

7 years ago

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

References

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

Author

robertylewis

Committer

mergify[bot]

Parents

3d512f79

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

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