www

commit 0306af85643281e588b686723a8b534a1a0bb1d5
parent 87abfa1085080e518ee9b2ba20fa480a7c7d3935
Author: Davide P. Cervone <dpvc@union.edu>
Date:   Tue, 17 Mar 2015 12:31:09 -0400

Use flushText() rather than adding the text by hand.

Diffstat:
M
unpacked/jax/output/CommonHTML/jax.js
 | 
2
+-

1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js
@@ -650,7 +650,7 @@
       }
       if (state.text !== "") {
         if (node.childNodes.length) {
-          HTML.addElement(node,"span",{className:state.className},[state.text]);
+          this.charList.flushText(node,state);
         } else {
           HTML.addText(node,state.text);
           node.className = state.className;