diff --git a/.devcontainer/build.sh b/.devcontainer/build.sh index f7b640c0..5ce292e9 100755 --- a/.devcontainer/build.sh +++ b/.devcontainer/build.sh @@ -1,3 +1,9 @@ #!/bin/sh +set -eu + +# A little helper script to rebuild the generated files using a known-good +# environment, so that we should all end up with the same results, and also +# no need to install any dependencies on the host machine. + cd $(dirname $0)/../ docker run --rm -v ${PWD}:/app $(docker build -q -f .devcontainer/Dockerfile .) diff --git a/.devcontainer/run.sh b/.devcontainer/run.sh index d698c90c..d086e1a5 100755 --- a/.devcontainer/run.sh +++ b/.devcontainer/run.sh @@ -1,3 +1,8 @@ #!/bin/sh +set -eu + +# A little helper script to run a shell in a known-good environment, so that +# developers can easily debug issues with the build process. + cd $(dirname $0)/../ docker run --rm -ti -v ${PWD}:/app $(docker build -q . -f .devcontainer/Dockerfile) /bin/bash