--- a/etc/abbrevs Tue Dec 29 19:11:23 2015 +0100
+++ b/etc/abbrevs Tue Dec 29 20:58:18 2015 +0100
@@ -1,5 +1,5 @@
(* additional abbreviations for syntactic completion *)
(*prevent replacement of very long arrows*)
-"--->" = "--->"
+"----->" = "----->"
"===>" = "===>"