Try using chown to fix file permissions

1 files changed, 4 insertions, 0 deletions

diff --git a/Jenkinsfile b/Jenkinsfile
index 4d31891..3254083 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -15,6 +15,10 @@ pipeline {
                     steps {
                         sh 'cask'
                         sh 'make html'
+                        // Because we're running in root, the public/ directory
+                        // isn't owned by the Jenkins user, meaning that
+                        // unstashing in a different stage fails.
+                        sh 'chown -R $(stat -c "%u" .):$(stat -c "%u" .) public'
                         stash includes: 'public/**', name: 'public_html'
                     }
                 }