Solves #400, this time hopefully for real.
The problem was that docker run doesn't actually run anything, it asks the docker daemon to do the job. Killing the parent process in case of a timeout wasn't doing the expected "termination on timeout" thing. By adding a switch hook to use docker kill to perform the cleanup works. Of course the runner needed to be named for this.
Solves #400, this time hopefully for real. The problem was that
docker rundoesn't actually run anything, it asks the docker daemon to do the job. Killing the parent process in case of a timeout wasn't doing the expected "termination on timeout" thing. By adding a switch hook to usedocker killto perform the cleanup works. Of course the runner needed to be named for this.