From 08278fa4e970ccda004839bca3c4cf345b662ad2 Mon Sep 17 00:00:00 2001
From: Sebastian Serth <Sebastian.Serth@hpi.de>
Date: Wed, 11 Nov 2020 18:16:07 +0100
Subject: [PATCH] Check for connection state before sending flush character

---
 app/assets/javascripts/editor/websocket.js | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/app/assets/javascripts/editor/websocket.js b/app/assets/javascripts/editor/websocket.js
index 09d64975..088e285f 100644
--- a/app/assets/javascripts/editor/websocket.js
+++ b/app/assets/javascripts/editor/websocket.js
@@ -4,7 +4,9 @@ CommandSocket = function(url, onOpen) {
   this.websocket.onopen = onOpen;
   this.websocket.onmessage = this.onMessage.bind(this);
   this.websocket.flush = function () {
-    this.send('\n');
+    if (this.readyState === this.OPEN) {
+        this.send('\n');
+    }
   }
 };