From dcc5ef2df65aafabde083f266ee164de2c716fa4 Mon Sep 17 00:00:00 2001
From: "Cheng-Han, Wu" <jackymaxj@gmail.com>
Date: Thu, 2 Jun 2016 01:06:55 +0800
Subject: [PATCH] Remove unnecessary editor refresh workaround because it
 already get fixed

---
 public/js/index.js | 1 -
 1 file changed, 1 deletion(-)

diff --git a/public/js/index.js b/public/js/index.js
index cb3bbcc4..25c84ad9 100644
--- a/public/js/index.js
+++ b/public/js/index.js
@@ -2502,7 +2502,6 @@ editor.on('changes', function (cm, changes) {
         viewportMargin = newViewportMargin;
         windowResize();
     }
-    editor.refresh();
 });
 editor.on('focus', function (cm) {
     for (var i = 0; i < onlineUsers.length; i++) {