diff --git a/IV/in-container b/IV/in-container index 368cca7..93632e2 100755 --- a/IV/in-container +++ b/IV/in-container @@ -1,8 +1,16 @@ #!/bin/bash set -euo pipefail -NAME=wm-mj-build +# Prefix the 'make <...>' with this script to build the artifact in an isolated +# container. This means host dependencies can only be Docker and a shell (to +# run this script). +# +# Usage: +# ./in-container make help +# ./in-container make -j mj-msc-full.pdf +# ... +NAME=wm-mj-build if [[ -z "$(docker images -q --filter "reference=$NAME")" ]]; then docker build -t "$NAME" - < Dockerfile fi