From 2ef77522e655264be3b154e085af6502e75911c0 Mon Sep 17 00:00:00 2001 From: rigzba21 Date: Thu, 5 Aug 2021 22:40:17 -0400 Subject: [PATCH] using rsync instead of mv to prevent accidental file deletion when bind mount a volume --- base-notebook/Dockerfile | 1 + base-notebook/start.sh | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/base-notebook/Dockerfile b/base-notebook/Dockerfile index 69414117..2e4b9419 100644 --- a/base-notebook/Dockerfile +++ b/base-notebook/Dockerfile @@ -42,6 +42,7 @@ RUN apt-get update --yes && \ wget \ ca-certificates \ sudo \ + rsync \ locales \ fonts-liberation \ run-one && \ diff --git a/base-notebook/start.sh b/base-notebook/start.sh index a63349fc..8b86a604 100755 --- a/base-notebook/start.sh +++ b/base-notebook/start.sh @@ -54,7 +54,7 @@ if [ "$(id -u)" == 0 ] ; then # (it could be mounted, and we shouldn't create it if it already exists) if [[ ! -e "/home/${NB_USER}" ]]; then echo "Relocating home dir to /home/${NB_USER}" - mv /home/jovyan "/home/${NB_USER}" || ln -s /home/jovyan "/home/${NB_USER}" + mkdir "/home/${NB_USER}" && rsync -avx /home/jovyan "/home/${NB_USER}" || ln -s /home/jovyan "/home/${NB_USER}" fi # if workdir is in /home/jovyan, cd to /home/${NB_USER} if [[ "${PWD}/" == "/home/jovyan/"* ]]; then