diff --git a/Jenkinsfile b/Jenkinsfile index 7f72724f25..4c00340b74 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -65,11 +65,9 @@ pipeline { failure { sh 'cat tools/check_format.txt' } - always { + cleanup { echo "Finished, deleting directory." deleteDir() - } - cleanup { echo "Clean up in post." cleanWs(cleanWhenNotBuilt: false, deleteDirs: true,