chore: use text-variant of ✝︎

[joneugster]

Second part of #5015, using emoji variant of unicode symbols for ✝︎.

---

(Partially) closes #5015

[joneugster]

Note: This appends the text-variant selector \u{FE0E} to all ✝︎ \u{271D}\u{FE0E}.

Need to wait for nightly-with-mathlib to include #5173 (i.e. should be 29/08/2024)

Implications:

• Batteries: TODO
• VSCode-lean4/infoview: not breaking, but chore: use text variant of ✝︎ vscode-lean4#520 applies the same changes.
• Mathilb: TODO

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c6feffa2bdabc0fbd75e3f8c2f9f681fbb7b41f5 --onto 9305049f1ef7309842806c2a994a2020bb32a71f. (2024-08-26 17:02:22)

[nomeata]

(Just labeling awaiting-author as per TODO list in first comment.)

[joneugster]

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