deleting user in docker run

runtimeverification · Sep 21, 2023 · 1644132 · 1644132
1 parent 6855fa0
commit 1644132
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml
@@ -44,7 +44,7 @@ jobs:
     runs-on: [self-hosted, linux, normal]
     continue-on-error: true
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v2
       - name: 'Set up Docker Test Image'
         env:
           BASE_OS: ubuntu
@@ -55,8 +55,6 @@ jobs:
           BENCHER_ADAPTER: json
         run: |
           set -euxo pipefail
-          USER=$(id -un)
-          GROUP=$(id -gn)
           docker run --name k-posting-profiling-tests-${GITHUB_SHA}                                   \
             --rm -it --detach                                                  \
             -e BENCHER_API_TOKEN=$BENCHER_API_TOKEN                            \
@@ -69,7 +67,6 @@ jobs:
             -e GITHUB_EVENT_NAME=$GITHUB_EVENT_NAME                            \
             -e GITHUB_REPOSITORY=$GITHUB_REPOSITORY                            \
             -e GITHUB_REF=$GITHUB_REF                                          \
-            --user ${USER}:${GROUP}                                            \
             --workdir /opt/workspace                                           \
             ${BASE_OS}:${BASE_DISTRO}
       - name: 'Copy K Framework'