etc/symbols
changeset 61972 a70b89a3e02e
parent 61964 37a0cbee00c2
child 62022 7a6ae107ec3c
--- a/etc/symbols	Tue Dec 29 23:40:04 2015 +0100
+++ b/etc/symbols	Tue Dec 29 23:50:44 2015 +0100
@@ -161,7 +161,7 @@
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
 \<longlongrightarrow>   code: 0x00290f  group: arrow  abbrev: .>  abbrev: --->
-\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: ---->
+\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: --->
 \<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
 \<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
 \<Lleftarrow>           code: 0x0021da  group: arrow  abbrev: <.