use dump when available instead of console.log

1 files changed, 7 insertions, 0 deletions

diff --git a/src/shell.html b/src/shell.html
index 404c9c11..17283c8f 100644
--- a/src/shell.html
+++ b/src/shell.html
@@ -36,6 +36,13 @@
             element.scrollTop = 99999; // focus on bottom
           };
         })(),
+        printErr: function(text) {
+          if (typeof dump == 'function') {
+            dump(text + '\n'); // fast, straight to the real console
+          } else {
+            console.log(text);
+          }
+        },
         canvas: document.getElementById('canvas'),
         setStatus: function(text) {
           if (Module.setStatus.interval) clearInterval(Module.setStatus.interval);