mathlib3
chore(category_theory/images): fix some minor problems
#2182

Merged

chore(category_theory/images): fix some minor problems #2182

mergify merged 4 commits into master from images_fixes

chore(category_theory/images): fix some minor problems

dd5b9d61

minor

d80d28cb

oops, misplaced comment

303e5819

kim-em requested a review from

jcommelin 5 years ago

kim-em added awaiting-review

jcommelin approved these changes on 2020-03-19

jcommelin removed awaiting-review

jcommelin added ready-to-merge

Merge branch 'master' into images_fixes

41a6bf8a

mergify merged a20f378f into master 5 years ago

mergify deleted the images_fixes branch 5 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone