areusch commented on code in PR #11184: URL: https://github.com/apache/tvm/pull/11184#discussion_r862073877
########## docker/with_the_same_user: ########## @@ -36,7 +36,12 @@ else rm /this_is_writable_file_system fi -getent group "${CI_BUILD_GID}" || addgroup --force-badname --gid "${CI_BUILD_GID}" "${CI_BUILD_GROUP}" +getent group "${CI_BUILD_GID}" || ( + # Ensure "${CI_BUILD_GROUP}" is not already some other gid inside container. + if grep -q "^${CI_BUILD_GROUP}:" /etc/group; then + CI_BUILD_GROUP="${CI_BUILD_GROUP}2" Review Comment: rather than do this, should we just set CI_BUILD_GROUP to the existing group? i think having two groups with identical gid is a bit weird, though cursory google does say it's supported. just curious if you tried this and didn't like that appraoch? -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: commits-unsubscr...@tvm.apache.org For queries about this service, please contact Infrastructure at: us...@infra.apache.org