2023-07-12 20:45:29 +02:00
|
|
|
#!/bin/sh
|
|
|
|
|
|
2023-07-23 16:39:02 +02:00
|
|
|
set -e
|
|
|
|
|
|
2023-07-12 20:45:29 +02:00
|
|
|
userID=$(id -u)
|
|
|
|
|
groupID=$(id -g)
|
|
|
|
|
|
|
|
|
|
mkdir -p ./build
|
|
|
|
|
|
2023-07-14 15:28:50 +02:00
|
|
|
echo "Building Docker image & Running build"
|
|
|
|
|
imageID=$(docker build -f docker/Dockerfile --build-arg UID="${userID}" --build-arg GID="${groupID}" --target builder -q .)
|
2023-07-12 20:45:29 +02:00
|
|
|
|
2023-07-14 15:28:50 +02:00
|
|
|
echo "Copying output"
|
|
|
|
|
docker run --rm -v ./build:/target "$imageID" cp /build/docker_launcher /target
|
2023-07-12 20:45:29 +02:00
|
|
|
|
|
|
|
|
echo "Removing image"
|
|
|
|
|
docker image rm "$imageID"
|
