1 files changed, 1 insertions, 1 deletions
diff --git a/src/shell.html b/src/shell.html
index 17283c8f..dad50b9f 100644
--- a/src/shell.html
+++ b/src/shell.html
@@ -37,7 +37,7 @@
           };
         })(),
         printErr: function(text) {
-          if (typeof dump == 'function') {
+          if (0) { // XXX disabled for safety typeof dump == 'function') {
             dump(text + '\n'); // fast, straight to the real console
           } else {
             console.log(text);