From 9942283db037dc1e68e2647343a8936d7b9f0693 Mon Sep 17 00:00:00 2001
From: Martin von Gagern <gagern@ma.tum.de>
Date: Tue, 7 Jul 2015 01:59:11 +0200
Subject: [PATCH] Fix incorrect symbol types

These symbols should have different types, according to symgroups.js
---
 src/symbols.js | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/symbols.js b/src/symbols.js
index 62b9ecb29..e5b1fd471 100644
--- a/src/symbols.js
+++ b/src/symbols.js
@@ -920,22 +920,22 @@ var symbols = {
         // AMS Delimiters
         "\\ulcorner": {
             font: "ams",
-            group: "textord",
+            group: "open",
             replace: "\u250c"
         },
         "\\urcorner": {
             font: "ams",
-            group: "textord",
+            group: "close",
             replace: "\u2510"
         },
         "\\llcorner": {
             font: "ams",
-            group: "textord",
+            group: "open",
             replace: "\u2514"
         },
         "\\lrcorner": {
             font: "ams",
-            group: "textord",
+            group: "close",
             replace: "\u2518"
         },
 
@@ -2172,12 +2172,12 @@ var symbols = {
         },
         "\\barwedge": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u22bc"
         },
         "\\veebar": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u22bb"
         },
         "\\odot": {
@@ -2207,12 +2207,12 @@ var symbols = {
         },
         "\\circledcirc": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u229a"
         },
         "\\boxdot": {
             font: "ams",
-            group: "textord",
+            group: "bin",
             replace: "\u22a1"
         },
         "\\bigtriangleup": {
@@ -2327,32 +2327,32 @@ var symbols = {
         },
         "\\uparrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u2191"
         },
         "\\Uparrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u21d1"
         },
         "\\downarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u2193"
         },
         "\\Downarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u21d3"
         },
         "\\updownarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u2195"
         },
         "\\Updownarrow": {
             font: "main",
-            group: "textord",
+            group: "rel",
             replace: "\u21d5"
         },
         "\\coprod": {
@@ -2447,7 +2447,7 @@ var symbols = {
         },
         "\\ldots": {
             font: "main",
-            group: "punct",
+            group: "inner",
             replace: "\u2026"
         },
         "\\cdots": {