From e20ee4546488b8a06f11838c7571a3cfb33d225d Mon Sep 17 00:00:00 2001
From: Sebastian Serth <Sebastian.Serth@hpi.de>
Date: Sat, 25 May 2024 20:11:56 +0200
Subject: [PATCH] Prevent duplicate error handling for WebSocket events

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

diff --git a/app/assets/javascripts/editor/editor.js.erb b/app/assets/javascripts/editor/editor.js.erb
index 3a9d1083..703844c3 100644
--- a/app/assets/javascripts/editor/editor.js.erb
+++ b/app/assets/javascripts/editor/editor.js.erb
@@ -215,6 +215,9 @@ var CodeOceanEditor = {
                     try {
                         return await callback();
                     } catch (error) {
+                        // WebSocket errors are handled in `showWebsocketError` already.
+                        if (error.target instanceof WebSocket) return;
+
                         console.error(JSON.stringify(error));
                         Sentry.captureException(JSON.stringify(error), {mechanism: {handled: false}});
                     }