etc/abbrevs
author wenzelm
Tue, 29 Dec 2015 22:41:22 +0100
changeset 61968 e13e70f32407
parent 61963 2548e7cc86fb
child 61970 6226261144d7
permissions -rw-r--r--
avoid immediate completion as ASCII versions that are still used;

(* additional abbreviations for syntactic completion *)

(*prevent replacement of very long arrows*)
"--->" = "--->"
"---->" = "---->"
"----->" = "----->"
"===>" = "===>"