Trying to fix ownership inside docker

runtimeverification · Sep 21, 2023 · 4704126 · 4704126
1 parent 89ac2e8
commit 4704126
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml
@@ -55,7 +55,6 @@ jobs:
           BENCHER_ADAPTER: json
         run: |
           set -euxo pipefail
-          chown root:root $(pwd)
           docker run --name k-posting-profiling-tests-${GITHUB_SHA}            \
             --rm -it --detach                                                  \
             -e BENCHER_API_TOKEN=$BENCHER_API_TOKEN                            \
@@ -76,6 +75,10 @@ jobs:
           workspace=$(pwd)
           docker cp ${workspace}/. k-posting-profiling-tests-${GITHUB_SHA}:/opt/workspace
 
+      - name: 'Changing directory ownership'
+        run: |
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c 'chown root:root /opt/workspace'
+
       - name: 'Setting up dependencies'
         run: |
           set -euxo pipefail