# HG changeset patch
# User wenzelm
# Date 1451425282 -3600
# Node ID e13e70f32407a3f82d6eb8f1a3cca49c3371f09f
# Parent  dd1f0caf27207d9d655d9ec23d68effd7bb66a1b
avoid immediate completion as ASCII versions that are still used;

diff -r dd1f0caf2720 -r e13e70f32407 etc/abbrevs
--- a/etc/abbrevs	Tue Dec 29 22:21:28 2015 +0100
+++ b/etc/abbrevs	Tue Dec 29 22:41:22 2015 +0100
@@ -1,5 +1,7 @@
 (* additional abbreviations for syntactic completion *)
 
 (*prevent replacement of very long arrows*)
+"--->" = "--->"
+"---->" = "---->"
 "----->" = "----->"
 "===>" = "===>"