diff --git a/scripts/docker/make.sh b/scripts/docker/make.sh index 88758c2a..13a4a4bb 100755 --- a/scripts/docker/make.sh +++ b/scripts/docker/make.sh @@ -102,12 +102,18 @@ filt= # arm takes forever so make it top priority [ ${a::3} == arm ] && nice= || nice=-n20 + # not sure if this is necessary or if inherit-annotations=false was enough, but won't hurt + readarray -t annot < <(awk > err; printf '%096d\n' $(seq 1 42))