From cbe1f5d2bb6ba9a8f6ef1261f0b7289f47358a58 Mon Sep 17 00:00:00 2001
From: Christophe Garion <tofgarion@runbox.com>
Date: Wed, 8 Mar 2023 13:50:13 +0100
Subject: [PATCH] [docker] add user ID and group for run script
---
scripts/run-docker.sh | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/scripts/run-docker.sh b/scripts/run-docker.sh
index 9d97b259..00dfa1bd 100755
--- a/scripts/run-docker.sh
+++ b/scripts/run-docker.sh
@@ -53,7 +53,7 @@ while true; do
done
# launch docker
-docker run -it --rm \
+docker run -it --rm --user $(id -u):$(id -g)\
--name "lustrec_docker_run" \
-v ${TMP_DIR}:/tmp -v ${PWD}:/home/opam/lustrec \
${CONTAINER_ID} $@
--
GitLab