diff --git a/UserManual.md b/UserManual.md index c9151e3..588ae34 100644 --- a/UserManual.md +++ b/UserManual.md @@ -588,6 +588,8 @@ docker run --rm -ti -v $PWD:/root ubuntu /bin/bash -xe <<(:) # get a new pipe +docker build - <<\EOF | + FROM debian:bullseye + RUN apt-get update && apt-get install -y build-essential +EOF +tee >(awk '/Successfully built/{print $3}' >&$pfd) # parse output to pipe +read tag <&$pfd # read tag back from pipe +exec {pfd}<&- # close pipe + +# Alternatively, you can use the -t option to docker build +# to give the built image a name to refer to later. But then +# you need to ensure that it does not conflict with any other +# images, and handle cases where multiple instances of the +# job attempt to update the tagged image. + +# If you want the image to be cleaned up on exit: +trap "docker rmi $tag" EXIT + +# Now use the image to build something: +docker run -i --rm \ + -v "$PWD:$PWD" \ + -w "$PWD" \ + -u $(id -u):$(id -g) \ + $tag /bin/bash -eux \ +<