Files
codeocean/app/controllers
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
..
2022-10-24 12:28:50 +02:00