delete mounting of host's user and group info (#3492)

runtimeverification · Jul 11, 2023 · 752c28d · 752c28d
1 parent 7fe67f1
commit 752c28d
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 4 deletions.
diff --git a/.github/actions/test-package/action.yml b/.github/actions/test-package/action.yml
@@ -83,8 +83,6 @@ runs:
         --detach                                                      \
         --workdir /opt/workspace                                      \
         -v "${workspace}:/opt/workspace"                              \
-        -v "/etc/passwd:/etc/passwd:ro"                               \
-        -v "/etc/group:/etc/group:ro"                                 \
         ${BASE_OS}:${BASE_DISTRO}
 
   - name: 'Test Package: ${{ inputs.os }}:${{ inputs.distro }}'

diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml
@@ -83,6 +83,4 @@ runs:
           --workdir /opt/workspace/${SUBDIR} \
           --user ${USER}:${GROUP}            \
           -v "$(pwd):/opt/workspace"         \
-          -v "/etc/passwd:/etc/passwd:ro"    \
-          -v "/etc/group:/etc/group:ro"      \
           runtimeverification/${TAG_NAME}