From a92c13ed719f82c1b5dccbce5dd5e7f5e997cbe3 Mon Sep 17 00:00:00 2001
From: Maximilian Grundke <maximiliangrundke@googlemail.com>
Date: Wed, 16 May 2018 14:35:08 +0200
Subject: [PATCH] Mute "unknown error" messages in Edge which occur after the
 socket was closed successfully

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

diff --git a/app/assets/javascripts/editor/editor.js.erb b/app/assets/javascripts/editor/editor.js.erb
index e16d37a7..00ce3fc7 100644
--- a/app/assets/javascripts/editor/editor.js.erb
+++ b/app/assets/javascripts/editor/editor.js.erb
@@ -552,6 +552,10 @@ configureEditors: function () {
   },
 
   showWebsocketError: function() {
+    if (window.navigator.userAgent.indexOf('Edge') > -1) {
+      // Mute errors in Microsoft Edge
+      return;
+    }
     $.flash.danger({
       text: $('#flash').data('message-failure')
     });