a05c58b6b read the arch list back out of the Dockerfile with
"$(dirname "$0")/Dockerfile", but build.sh already does
cd "$(dirname "$0")" near the top. The dirname is therefore applied
twice, so every invocation by a path other than ./build.sh from inside
docker/ died before reaching docker build:
$ bash wt_r5748/docker/build.sh
sed: can't read wt_r5748/docker/Dockerfile: No such file or directory
EXIT=2
set -euo pipefail turns the sed failure into an abort, so this broke the
whole script rather than just the banner it was meant to print.
Use a bare filename, which is what the rest of the script already does
(the docker build context below is a bare "."). Verified from the
workspace root, from an absolute path, and from docker/ itself: all
three now print
arch list 7.5;8.0;8.6;8.9;9.0;10.0;12.0+PTX
18260a2729