Skip to content
This repository has been archived by the owner on Jun 16, 2021. It is now read-only.

Commit

Permalink
Remove operators "|||" from the dictionary
Browse files Browse the repository at this point in the history
* "|||" does not seem to be used as a programming language operator.
* For (stretchy) fences, U+2980 is more appropriate than "|||"

w3c/mathml#143
w3c/mathml#176
  • Loading branch information
fred-wang committed May 7, 2020
1 parent a7d0263 commit 9f203ff
Showing 1 changed file with 0 additions and 7 deletions.
7 changes: 0 additions & 7 deletions unicode.xml
Original file line number Diff line number Diff line change
Expand Up @@ -1827,13 +1827,6 @@ Barbara Beeton for the STIX project
<operator-dictionary priority="20" form="postfix" fence="true" lspace="0" rspace="0"/>
<description>MULTIPLE CHARACTER OPERATOR: ||</description>
</character>
<character id="U0007C-0007C-0007C" dec="124-124-124" image="none">
<unicodedata/>
<operator-dictionary priority="270" form="infix" lspace="3" rspace="3" fence="true"/>
<operator-dictionary priority="20" form="prefix" fence="true" lspace="0" rspace="0"/>
<operator-dictionary priority="20" form="postfix" fence="true" lspace="0" rspace="0"/>
<description>MULTIPLE CHARACTER OPERATOR: |||</description>
</character>
<character id="U0007D" dec="125" mode="math" type="closing">
<unicodedata category="Pe" combclass="0" bidi="ON" mirror="Y" unicode1="CLOSING CURLY BRACKET" mathclass="C" alias="closing brace;closing curly bracket"/>
<afii>007D</afii>
Expand Down

0 comments on commit 9f203ff

Please sign in to comment.