minor bugfix

diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js
index d0b5ce21768f22ae8ffaf6671f68fc2e8779a10d..5cd0fef8211a0f7d4d499ce8860ee5ef48fb8a25 100644 (file)
--- a/matitaB/matita/matitaweb.js
+++ b/matitaB/matita/matitaweb.js
@@ -85,8 +85,8 @@ function pressmesg(w,e)
 {
    debug(w + '  keyCode=' + keyval(e.keyCode) +
                  ' which=' + keyval(e.which) +
-                 ' charCode=' + keyval(e.charCode));
-   debug('          shiftKey='+e.shiftKey
+                 ' charCode=' + keyval(e.charCode) +
+                '\n          shiftKey='+e.shiftKey
              + ' ctrlKey='+e.ctrlKey
              + ' altKey='+e.altKey
              + ' metaKey='+e.metaKey);
@@ -112,6 +112,8 @@ function keypress(e)
 function debug(txt)
 {
         // internet explorer (v.9) doesn't work with innerHTML
+       // but google chrome's innerText is, in a sense, "write only"
+       // what should we do?
         logarea.innerText = txt + "\n" + logarea.innerText;
 }