From 0306af85643281e588b686723a8b534a1a0bb1d5 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Tue, 17 Mar 2015 12:31:09 -0400
Subject: [PATCH] Use flushText() rather than adding the text by hand.

---
 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
index 33439b40a..3dfccfc3a 100644
--- 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;