Files
codeocean/app
Sebastian Serth 50a4707f65 Prevent duplicated WebSocket close for client_kill
Our investigation in CODEOCEAN-TV showed that we might attempt to close the WebSocket connection twice, if learners press the stop button. With this commit, we fix that issue.
2023-09-08 00:16:12 +02:00
..