# HG changeset patch
# User wenzelm
# Date 1396804594 -7200
# Node ID ee0f7cfb7bba822388b738517bb68da301dca7d1
# Parent  681717041f550de2f71fbaa3d462528537fdc9ab
removed abbrev "<-" again (see c771f0fe28d1) due to conflict with important "<->" and "<-->";

diff -r 681717041f55 -r ee0f7cfb7bba etc/symbols
--- a/etc/symbols	Sun Apr 06 17:19:08 2014 +0200
+++ b/etc/symbols	Sun Apr 06 19:16:34 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: <.  abbrev: <-
+\<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
 \<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->