From b40e4e96e85103c7072985990c6b541371fd5a48 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 23 Mar 2012 10:11:15 +0000 Subject: [PATCH] Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals correctly. --- matitaB/matita/html/matitaweb.js | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js index cec0bb3ba..20d0fec43 100644 --- a/matitaB/matita/html/matitaweb.js +++ b/matitaB/matita/html/matitaweb.js @@ -420,8 +420,9 @@ function populate_goalarray(menv) var tmp_goallist = ""; for (i = 0; i < menv.length; i++) { metano = menv[i].getAttribute("number"); - metaname = menv[i].childNodes[0].childNodes[0].data; - goal = menv[i].childNodes[1].childNodes[0].data; + // item 0 = , item 1 = + metaname = menv[i].childNodes[0].childNodes[0].wholeText; + goal = menv[i].childNodes[1].childNodes[0].wholeText; debug ("found meta n. " + metano); debug ("found goal\nBEGIN" + goal + "\nEND"); goalarray[metano] = goal; -- 2.39.2