diff --git a/docs/_includes/repl.html b/docs/_includes/repl.html
index e769643b..8a946d59 100644
--- a/docs/_includes/repl.html
+++ b/docs/_includes/repl.html
@@ -63,7 +63,7 @@
function output(text) {
var output_box = document.getElementById("output");
- output_box.value += text.replace('stdin:', '') + "\n";
+ output_box.value += text + "\n";
// scroll to bottom
output_box.scrollTop = output_box.scrollHeight;
}