diff -r d92eb5c3960d -r c771f0fe28d1 etc/symbols
--- a/etc/symbols	Thu Apr 03 14:54:17 2014 +0200
+++ b/etc/symbols	Thu Apr 03 15:40:31 2014 +0200
@@ -154,7 +154,7 @@
 \<rat>                  code: 0x00211a  group: letter
 \<real>                 code: 0x00211d  group: letter
 \<int>                  code: 0x002124  group: letter
-\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
+\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.  abbrev: <-
 \<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->