etc/symbols
changeset 73447 2200a19cac72
parent 73446 d1c4c2395650
child 73450 c5315b89c1bf
--- a/etc/symbols	Wed Mar 17 22:24:57 2021 +0100
+++ b/etc/symbols	Thu Mar 18 12:41:17 2021 +0100
@@ -381,6 +381,7 @@
 \<Zrres>                code: 0x0025B7  group: Z_Notation  group: relation
 \<Znrres>               code: 0x002A65  group: Z_Notation  group: relation
 \<Zspot>                code: 0x002981  group: Z_Notation  group: punctuation
+\<Zproject>             code: 0x002A21  group: Z_Notation  group: operator
 \<Ztypecolon>           code: 0x002982  group: Z_Notation  group: relation
 \<Zhide>                code: 0x0029F9  group: Z_Notation  group: operator
 \<Zcat>                 code: 0x002040  group: Z_Notation  group: operator