From 159cd44d7188986b19b45a692cd9dfc00a610c25 Mon Sep 17 00:00:00 2001
From: Tim Neumann <mail@timnn.me>
Date: Wed, 11 Jan 2017 12:58:24 +0100
Subject: [PATCH] fix nightly highlighting

---
 static/web.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/static/web.js b/static/web.js
index 1db4216..10a42ff 100644
--- a/static/web.js
+++ b/static/web.js
@@ -549,12 +549,12 @@
                 return '<span class=ansi-' + COLOR_CODES[+colorCode] + '>' + text + '</span>';
             }).replace(/\x1b\[1m([^\x1b]*)(?:\x1b\(B)?\x1b\[0?m/g, function(original, text) {
                 return "<strong>" + text + "</strong>";
-            }).replace(/(?:\x1b\(B)?\x1b\[0m/g, '');
+            }).replace(/(?:\x1b\(B)?\x1b\[0?m/g, '');
     }
 
     //This affects how mouse acts on the program output.
     //Screenshots here: https://github.com/rust-lang/rust-playpen/pull/192#issue-145465630
-    //If mouse hovers on eg. "<anon>:3", temporarily show that line(3) into view by 
+    //If mouse hovers on eg. "<anon>:3", temporarily show that line(3) into view by
     //selecting it entirely and move editor's cursor to the beginning of it;
     //Moves back to original view when mouse moved away.
     //If mouse left click on eg. "<anon>:3" then the editor's cursor is moved