Fix Unicode bigcup (#1836)

This commit is contained in:
Ron Kok
2019-01-20 09:38:14 -08:00
committed by Erik Demaine
parent 062a28f35a
commit 2cd37ae7c3

View File

@@ -273,7 +273,7 @@ const singleCharBigOps: {[string]: string} = {
"\u22c0": "\\bigwedge",
"\u22c1": "\\bigvee",
"\u22c2": "\\bigcap",
"\u22c3": "\\bigcap",
"\u22c3": "\\bigcup",
"\u2a00": "\\bigodot",
"\u2a01": "\\bigoplus",
"\u2a02": "\\bigotimes",