chore(unicode): improve arrows #1373
mergify
merged
7 commits into
master
from
improve-arrows
chore(unicode): improve arrows
9000e0cd
jcommelin
commented
on 2019-08-30
grammar
79de3413
moar
a727bba2
Merge branch 'master' of github.com:leanprover-community/mathlib
2ac103b5
Merge branch 'improve-arrows' of github.com:leanprover-community/mathlib
9385ccd7
Merge branch 'master' into improve-arrows
21c0a68c
cipher1024
approved these changes
on 2019-08-30
jcommelin
approved these changes
on 2019-08-30
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into improve-arrows
2dc6b378
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub