mathlib3
doc(topology/basic): add a few doc strings [skip ci]
#1775

Merged

doc(topology/basic): add a few doc strings [skip ci] #1775

mergify merged 3 commits into master from topology-docs

doc(topology/basic): add a few doc strings

5bea45a3

urkud changed the title ~~doc(topology/basic): add a few doc strings~~ doc(topology/basic): add a few doc strings [ci skip] 6 years ago

urkud changed the title ~~doc(topology/basic): add a few doc strings [ci skip]~~ doc(topology/basic): add a few doc strings [skip ci] 6 years ago

sgouezel commented on 2019-12-04

Apply suggestions from code review

e3487c9f

sgouezel added ready-to-merge

sgouezel approved these changes on 2019-12-04

Merge branch 'master' into topology-docs

b5b6ff6a

mergify merged 43531676 into master 6 years ago

mergify deleted the topology-docs branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone