From 962eda41daa94e67aa09a23e4f02b69329ae9bd0 Mon Sep 17 00:00:00 2001 From: Shish Date: Sun, 19 Jan 2025 23:52:50 +0000 Subject: [PATCH] [docker] exit early if build fails If the build fails, don't then attempt to run the container-which-wasn't-built --- .devcontainer/build.sh | 6 ++++++ .devcontainer/run.sh | 5 +++++ 2 files changed, 11 insertions(+) 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