#!/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_DIR="$(CDPATH= cd -- "$(dirname -- "$0")" && pwd)" DEVCONTAINER_DIR="${SCRIPT_DIR%/scripts}" ROOT_DIR="${DEVCONTAINER_DIR%/.devcontainer}" OUT_FILE="${DEVCONTAINER_DIR}/Dockerfile" echo "Adding base Dockerfile from $ROOT_DIR..." echo "# DO NOT MODIFY THIS FILE DIRECTLY. IT IS AUTO-GENERATED BY .devcontainer/scripts/generate-configs.sh" > "$OUT_FILE" echo "" >> "$OUT_FILE" echo "# ---/Dockerfile---" >> "$OUT_FILE" cat "${ROOT_DIR}/Dockerfile" >> "$OUT_FILE" echo "" >> "$OUT_FILE" echo "# ---/resources/devcontainer-Dockerfile---" >> "$OUT_FILE" echo "" >> "$OUT_FILE" echo "Adding devcontainer-Dockerfile from $DEVCONTAINER_DIR/resources..." cat "${DEVCONTAINER_DIR}/resources/devcontainer-Dockerfile" >> "$OUT_FILE" echo "Generated $OUT_FILE using root dir $ROOT_DIR" >&2 echo "Done."