From 29ad780853d4ff1129e210d65c16a607169b50e3 Mon Sep 17 00:00:00 2001 From: Someone-dQw4w9WgXcQ Date: Thu, 27 Jul 2023 13:28:03 +0100 Subject: [PATCH] Remove .replace('stdin:', '') --- docs/_includes/repl.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; }