# HG changeset patch
# User wenzelm
# Date 1616430487 -3600
# Node ID 86b900eff9bf9f4f6786bf05655049c435274352
# Parent  090add96f5f90764fb13d534cc7213340ec233bd
clarified group (but hard to tell);

diff -r 090add96f5f9 -r 86b900eff9bf etc/symbols
--- a/etc/symbols	Mon Mar 22 17:24:42 2021 +0100
+++ b/etc/symbols	Mon Mar 22 17:28:07 2021 +0100
@@ -300,9 +300,9 @@
 \<succ>                 code: 0x00227b  group: relation
 \<preceq>               code: 0x00227c  group: relation
 \<succeq>               code: 0x00227d  group: relation
-\<parallel>             code: 0x002225  group: punctuation  abbrev: ||
-\<interleave>           code: 0x002af4  group: punctuation  abbrev: ||
-\<sslash>               code: 0x002afd  group: punctuation  abbrev: ||
+\<parallel>             code: 0x002225  group: relation  abbrev: ||
+\<interleave>           code: 0x002af4  group: relation  abbrev: ||
+\<sslash>               code: 0x002afd  group: relation  abbrev: ||
 \<bar>                  code: 0x0000a6  group: punctuation  abbrev: ||
 \<bbar>                 code: 0x002aff  group: punctuation  abbrev: ||
 \<plusminus>            code: 0x0000b1  group: operator