From fe13349850bceb6670ee65d54a6e140c5cddda92 Mon Sep 17 00:00:00 2001
From: Cassie Tarakajian <ctarakajian@gmail.com>
Date: Thu, 6 Oct 2016 15:48:45 -0400
Subject: [PATCH] make autorefresh time a little longer

---
 client/modules/IDE/components/Editor.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/client/modules/IDE/components/Editor.js b/client/modules/IDE/components/Editor.js
index 1e08d2b6..f5dfeff6 100644
--- a/client/modules/IDE/components/Editor.js
+++ b/client/modules/IDE/components/Editor.js
@@ -65,7 +65,7 @@ class Editor extends React.Component {
       }
     });
 
-    this._cm.on('change', debounce(200, () => {
+    this._cm.on('change', debounce(400, () => {
       this.props.setUnsavedChanges(true);
       this.props.updateFileContent(this.props.file.name, this._cm.getValue());
       if (this.props.autorefresh && this.props.isPlaying) {