#!/bin/sh # Generator for .devcontainer/Dockerfile # Combines the root /Dockerfile (with some COPY lines removed) and # the dev-only stage in .devcontainer/resources/devcontainer-Dockerfile. # Run this script after modifying the resource Dockerfile to refresh # the final .devcontainer/Dockerfile used by the devcontainer. echo "Generating .devcontainer/Dockerfile" SCRIPT_PATH=$(set -- "$0"; dirname -- "$1") SCRIPT_DIR=$(cd "$SCRIPT_PATH" && pwd -P) DEVCONTAINER_DIR="${SCRIPT_DIR%/scripts}" ROOT_DIR="${DEVCONTAINER_DIR%/.devcontainer}" OUT_FILE="${DEVCONTAINER_DIR}/Dockerfile" echo "Adding base Dockerfile from $ROOT_DIR and merging to devcontainer-Dockerfile" { echo "# DO NOT MODIFY THIS FILE DIRECTLY. IT IS AUTO-GENERATED BY .devcontainer/scripts/generate-configs.sh" echo "" echo "# ---/Dockerfile---" cat "${ROOT_DIR}/Dockerfile" echo "" echo "# ---/resources/devcontainer-Dockerfile---" echo "" cat "${DEVCONTAINER_DIR}/resources/devcontainer-Dockerfile" } > "$OUT_FILE" echo "Generated $OUT_FILE using root dir $ROOT_DIR" echo "Done."