diff --git a/app/run_docker.sh b/app/run_docker.sh index 547be6e3d..cd5364739 100755 --- a/app/run_docker.sh +++ b/app/run_docker.sh @@ -135,6 +135,15 @@ if [[ -n "$GIT_REPO_DIR" ]]; then DOCKER_ARGS+=( -v "$GIT_REPO_DIR/src:/src" ) fi + # Prefer ./externals (plural) as requested; fall back to ./external + if [[ -d "$GIT_REPO_DIR/externals" ]]; then + DOCKER_ARGS+=( -v "$GIT_REPO_DIR/externals:/repo/external" ) + echo "Mounting repo externals from $GIT_REPO_DIR/externals -> /repo/external" + elif [[ -d "$GIT_REPO_DIR/external" ]]; then + DOCKER_ARGS+=( -v "$GIT_REPO_DIR/external:/repo/external" ) + echo "Mounting repo external from $GIT_REPO_DIR/external -> /repo/external" + fi + if [[ -z "$WORKDIR_IN_CONTAINER" ]]; then WORKDIR_IN_CONTAINER="/repo" fi