From 258d99a4cb1722a961240e10a2806aefccb95ede Mon Sep 17 00:00:00 2001
From: Tom Willemse <tom@ryuslash.org>
Date: Fri, 9 Oct 2020 23:57:49 -0700
Subject: [PATCH] Try using chown to fix file permissions

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

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'
                     }
                 }