diff --git a/Jenkinsfile b/Jenkinsfile
index 991c940ad6..76630393e6 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -16,6 +16,8 @@ ssh -tt -o ConnectTimeout=30 -o ServerAliveInterval=30 -o ServerAliveCountMax=3
 
 set -e
 
+shopt -s huponexit # kill all child processes when the shell exits
+
 export CI=1
 export PYTHONWARNINGS=error
 export LOGPRINT=debug