chore: Make hadolint happy for mkdir -p -m …

coq-community · Mar 8, 2024 · 777024f · 777024f
1 parent 510d5d2
commit 777024f
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 0 deletions.
diff --git a/base/bare/Dockerfile b/base/bare/Dockerfile
@@ -54,6 +54,7 @@ ARG guest_uid=1000
 ARG guest_gid=${guest_uid}
 
 # Add Coq group and user with sudo perms
+# hadolint ignore=SC2174
 RUN groupadd -g ${guest_gid} coq \
   && useradd --no-log-init -m -s /bin/bash -g coq -G sudo -p '' -u ${guest_uid} coq \
   # Create dirs for user scripts

diff --git a/base/dual/Dockerfile b/base/dual/Dockerfile
@@ -48,6 +48,7 @@ ARG guest_uid=1000
 ARG guest_gid=${guest_uid}
 
 # Add Coq group and user with sudo perms
+# hadolint ignore=SC2174
 RUN groupadd -g ${guest_gid} coq \
   && useradd --no-log-init -m -s /bin/bash -g coq -G sudo -p '' -u ${guest_uid} coq \
   # Create dirs for user scripts

diff --git a/base/single/Dockerfile b/base/single/Dockerfile
@@ -48,6 +48,7 @@ ARG guest_uid=1000
 ARG guest_gid=${guest_uid}
 
 # Add Coq group and user with sudo perms
+# hadolint ignore=SC2174
 RUN groupadd -g ${guest_gid} coq \
   && useradd --no-log-init -m -s /bin/bash -g coq -G sudo -p '' -u ${guest_uid} coq \
   # Create dirs for user scripts