Hashtags getting backslashes now

JonasKappa · Nov 16, 2019 · e70bbf7 · e70bbf7
1 parent a824e01
commit e70bbf7
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/FFC/ffc.js b/src/FFC/ffc.js
@@ -185,6 +185,8 @@ function checkForTokenWithDifferentMeaningInLaTeX(swapDollar, label) {
                 res = res.concat('$\\mid$');
             } else if (l == '-') {
                 res = res.concat('$\\relbar$');
+            } else if (l == '#') {
+                res = res.concat('\\#');
             } else {
                 res = res.concat(l);
             }
@@ -201,6 +203,8 @@ function checkForTokenWithDifferentMeaningInLaTeX(swapDollar, label) {
             return '$\\mid$';
         } else if (label == '-') {
             return '$\\relbar$';
+        } else if (label == '#') {
+            return '\\#';
         } else {
             return label;
         }