mathlib3
doc(docs/contribute, meta/expr): sectioning doc strings
#1723
Merged

doc(docs/contribute, meta/expr): sectioning doc strings #1723

mergify merged 4 commits into master from doc-update
robertylewis
robertylewis doc(docs/contribute, meta/expr): explain sectioning doc strings and s…
13c630b5
cipher1024
cipher1024 commented on 2019-11-21
robertylewis updates
cf6c9fc7
sgouezel sgouezel added ready-to-merge
sgouezel
sgouezel approved these changes on 2019-11-29
robertylewis
mergify[bot] Merge branch 'master' into doc-update
2dfda324
mergify[bot] Merge branch 'master' into doc-update
d98fca71
mergify mergify merged e68b2be5 into master 6 years ago
mergify mergify deleted the doc-update branch 6 years ago

Login to write a write a comment.

Login via GitHub

Assignees
No one assigned
Labels
Milestone