From f579737d20391ad53c85318913aa86185f13a2e7 Mon Sep 17 00:00:00 2001 From: =?utf8?q?=EC=98=A4=ED=98=95=EC=84=9D/=EB=8F=99=EC=9E=91=EC=A0=9C?= =?utf8?q?=EC=96=B4Lab=28SR=29/Staff=20Engineer/=EC=82=BC=EC=84=B1?= =?utf8?q?=EC=A0=84=EC=9E=90?= Date: Mon, 26 Nov 2018 10:06:56 +0900 Subject: [PATCH] Delete docker_helper file (#3689) Delete docker_helper script file: not used any more Signed-off-by: Hyeongseok Oh --- scripts/docker_helper | 33 --------------------------------- 1 file changed, 33 deletions(-) delete mode 100644 scripts/docker_helper diff --git a/scripts/docker_helper b/scripts/docker_helper deleted file mode 100644 index 37ec9fc..0000000 --- a/scripts/docker_helper +++ /dev/null @@ -1,33 +0,0 @@ -# Newly created files during docker run can have different ownership. -# This may cause some problems, for example, some jenkins slaves or developers -# can't remove built files due to lack of permission. -# To address this issue, let's change owner of all files and subdirector -# to owner of host directory. -# -# Parameters: -# $1 : host directory -# $2 : docker directory -# -# Requires following variables defined -# DOCKER_RUN_OPTS, DOCKER_ENV_VARS, DOCKER_VOLUMES, DOCKER_IMAGE_NAME -function restore_ownership() { - if [ -z "$1" ] - then - echo "Requires host path" - exit 1 - fi - _HOST_DIR=$1 - - if [ -z "$2" ] - then - echo "Requires docker path" - exit 1 - fi - - _DOCKER_DIR=$2 - - _OWNER_UID=$(stat -c "%u" $_HOST_DIR) - _OWNER_GID=$(stat -c "%g" $_HOST_DIR) - CMD="chown -R $_OWNER_UID:$_OWNER_GID $_DOCKER_DIR" - docker run $DOCKER_RUN_OPTS $DOCKER_ENV_VARS $DOCKER_VOLUMES $DOCKER_IMAGE_NAME $CMD -} -- 2.7.4