From 9f203ff7c8adc19153f3855899e8c918cf5a5e18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Wang?= Date: Thu, 7 May 2020 13:41:57 +0200 Subject: [PATCH] Remove operators "|||" from the dictionary * "|||" does not seem to be used as a programming language operator. * For (stretchy) fences, U+2980 is more appropriate than "|||" https://github.com/mathml-refresh/mathml/issues/143 https://github.com/mathml-refresh/mathml/issues/176 --- unicode.xml | 7 ------- 1 file changed, 7 deletions(-) diff --git a/unicode.xml b/unicode.xml index dd9a37d..a51f4dd 100644 --- a/unicode.xml +++ b/unicode.xml @@ -1827,13 +1827,6 @@ Barbara Beeton for the STIX project MULTIPLE CHARACTER OPERATOR: || - - - - - - MULTIPLE CHARACTER OPERATOR: ||| - 007D