From e4525bca361d65a7af3e2b8c8194026bb1f51fd5 Mon Sep 17 00:00:00 2001
From: Maximilian Grundke <maximiliangrundke@googlemail.com>
Date: Wed, 16 May 2018 14:37:13 +0200
Subject: [PATCH] Cleanly close websocket

---
 app/assets/javascripts/editor/websocket.js.erb | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/app/assets/javascripts/editor/websocket.js.erb b/app/assets/javascripts/editor/websocket.js.erb
index baba623d..1d0e2b25 100644
--- a/app/assets/javascripts/editor/websocket.js.erb
+++ b/app/assets/javascripts/editor/websocket.js.erb
@@ -108,5 +108,5 @@ CommandSocket.prototype.flush = function() {
  */
 CommandSocket.prototype.killWebSocket = function() {
   this.websocket.flush();
-  this.websocket.close();
-};
\ No newline at end of file
+  this.websocket.close(1000);
+};