diff -r 720fa884656e -r a70b89a3e02e etc/symbols
--- 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: <.