From 1c6bc54504da1d2ce52df1775c6c44ad11bd0e33 Mon Sep 17 00:00:00 2001
From: Christian Poessinger <christian@poessinger.com>
Date: Mon, 14 Jan 2019 21:51:59 +0100
Subject: Jenkins: allow regular user to clean 'build/' directory

---
 Jenkinsfile | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Jenkinsfile')

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 */
         }
     }
-- 
cgit v1.2.3