From 91cb2a3391b511a9c94b49dfb80151ac8f550ee7 Mon Sep 17 00:00:00 2001
From: Ralf Teusner <ralf.teusner@hpi.de>
Date: Thu, 15 Oct 2015 15:27:57 +0200
Subject: [PATCH] set correct newlines in output

---
 app/assets/javascripts/editor.js | 1 +
 1 file changed, 1 insertion(+)

diff --git a/app/assets/javascripts/editor.js b/app/assets/javascripts/editor.js
index 279e7c27..160cf315 100644
--- a/app/assets/javascripts/editor.js
+++ b/app/assets/javascripts/editor.js
@@ -1161,6 +1161,7 @@ $(function() {
         return;
       }
       //msg.data = msg.data.replace(/(\r\n|\n|\r)/gm, "<br />");
+      msg.data = msg.data.replace(/(\r)/gm, "\n");
       var stream = {};
       stream[msg.stream] = msg.data;
       printOutput(stream, true, 0);