-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore: use text-variant of ✝︎ #5174
Conversation
Note: This appends the text-variant selector Need to wait for Implications:
|
Mathlib CI status (docs):
|
362f60c
to
2fca0e8
Compare
6e36fee
to
9b82553
Compare
9b82553
to
268b60a
Compare
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
(Just labeling |
I am not 100% confident, that this will not cause problems anywhere, and I don't strictly need this change. (having emojis marked as emojis means I can load the emoji font behind the non-emoji one and everything renders fine). So I'm going to close this PR |
Second part of #5015, using emoji variant of unicode symbols for ✝︎.
(Partially) closes #5015