--- 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*)
+"--->" = "--->"
+"---->" = "---->"
"----->" = "----->"
"===>" = "===>"