chore: remove rial symbol (#525)

Closes #522.
leanprover · Sep 10, 2024 · d64bd91 · d64bd91
1 parent 63caac0
commit d64bd91
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json
@@ -1120,7 +1120,6 @@
     "rrbracket": "〛",
     "rangle": "⟩",
     "rq": "’",
-    "rial": "﷼",
     "rightarrowtail": "↣",
     "rightarrow": "→",
     "rightharpoondown": "⇁",