When docker kills the computation, only sometimes the user gets the message (in stderr) that the process has been killed. The backend should monitor the killing (docker events?) and generate a meaningful error message for the user.
When docker kills the computation, only sometimes the user gets the message (in stderr) that the process has been killed.
The backend should monitor the killing (docker events?) and generate a meaningful error message for the user.