Matitaweb: added preliminary support for interactive disambiguation.

[helm.git] / matitaB / matita / matitaweb.js

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index fedaaf7fbde482deb54024c25aa65e5834a816bf..ccb2f37445fabf8e38332df2fc714e9d5fffbf6e 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -233,7 +233,7 @@ function debug(txt)
        // but google chrome's innerText is, in a sense, "write only"
        // what should we do?
         // logarea.innerText = txt + "\n" + logarea.innerText;
-        logtxt = logtxt + "\n" + txt;
+        logtxt = /* logtxt + "\n" +*/ txt;
 }
 
 function showLog() {