From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Fri, 23 Mar 2012 10:11:15 +0000 (+0000)
Subject: Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
X-Git-Tag: make_still_working~1837
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b40e4e96e85103c7072985990c6b541371fd5a48;hp=b503649d75bd4cb8edf87418abfd56bf06c18cfd;p=helm.git

Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
correctly.
---

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 = <metaname>, item 1 = <goal>
+	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;