summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2023-02-21 14:44:21 +0000
committerDavid Allsopp <david.allsopp@metastack.com>2023-02-21 14:44:21 +0000
commit72062d5ae500aab22e44c9b348f5c5e5f1aed9b2 (patch)
treef61a463b465321d72dde75bc8221d0f6aa99e608 /tools
parent10ef09e1f3bae325e7f561d0cacf038a2fbc0094 (diff)
downloadocaml-72062d5ae500aab22e44c9b348f5c5e5f1aed9b2.tar.gz
Report all post-build failures
Rather than just reporting un-prefixed symbol names, also report undefined variables.
Diffstat (limited to 'tools')
-rwxr-xr-xtools/ci/actions/runner.sh12
1 files changed, 9 insertions, 3 deletions
diff --git a/tools/ci/actions/runner.sh b/tools/ci/actions/runner.sh
index 10746cda37..f64c2ce4e0 100755
--- a/tools/ci/actions/runner.sh
+++ b/tools/ci/actions/runner.sh
@@ -63,13 +63,19 @@ Build () {
else
script --return --command "$MAKE_WARN" build.log
fi
- echo Ensuring that all names are prefixed in the runtime
- ./tools/check-symbol-names runtime/*.a otherlibs/*/lib*.a
+ failed=0
if grep -Fq ' warning: undefined variable ' build.log; then
echo Undefined Makefile variables detected
- exit 1
+ failed=1
fi
rm build.log
+ echo Ensuring that all names are prefixed in the runtime
+ if ! ./tools/check-symbol-names runtime/*.a otherlibs/*/lib*.a ; then
+ failed=1
+ fi
+ if ((failed)); then
+ exit 1
+ fi
}
Test () {