Jenkins: allow regular user to clean 'build/' directory

1 files changed, 3 insertions, 0 deletions

diff --git a/Jenkinsfile b/Jenkinsfile
index fc08eff2..32ddcd65 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -55,6 +55,9 @@ pipeline {
     post {
         always {
             echo 'One way or another, I have finished'
+            // the 'build' directory got elevated permissions during the build
+            // cdjust permissions so it can be cleaned up by the regular user
+            sh 'sudo chmod -R 777 build/'
             deleteDir() /* cleanup our workspace */
         }
     }