diff --git a/ci/Jenkinsfile.prs b/ci/Jenkinsfile.prs index 59b92e679..c56cd929e 100644 --- a/ci/Jenkinsfile.prs +++ b/ci/Jenkinsfile.prs @@ -75,6 +75,7 @@ pipeline { post { success { script { github.notifyPR(true) } } failure { script { github.notifyPR(false) } } + always { cleanWs() } } // post } // pipeline