Merge pull request #299 from gagern/delimiters

Provide more delimiters
2025-10-15 15:58:40 +00:00 · 2015-07-19 21:14:13 -06:00
parent 2600587f78 7c8ea80638
commit 476eebf3c5
3 changed files with 35 additions and 1 deletions
--- a/src/symbols.js
+++ b/src/symbols.js
@@ -1947,6 +1947,11 @@ var symbols = {
            group: "open",
            replace: "\u2223"
        },
+        "\\lVert": {
+            font: "main",
+            group: "open",
+            replace: "\u2225"
+        },
        ")": {
            font: "main",
            group: "close"
@@ -1973,6 +1978,11 @@ var symbols = {
            group: "close",
            replace: "\u2223"
        },
+        "\\rVert": {
+            font: "main",
+            group: "close",
+            replace: "\u2225"
+        },
        "=": {
            font: "main",
            group: "rel"