diff options
| -rwxr-xr-x | tools/ci.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/ci.sh b/tools/ci.sh index 815e728757..4ff4ba35ba 100755 --- a/tools/ci.sh +++ b/tools/ci.sh @@ -515,6 +515,8 @@ function ci_unix_macos_build { #make ${MAKEOPTS} -C ports/unix deplibs make ${MAKEOPTS} -C ports/unix # check for additional compiler errors/warnings + make ${MAKEOPTS} -C ports/unix VARIANT=dev submodules + make ${MAKEOPTS} -C ports/unix VARIANT=dev make ${MAKEOPTS} -C ports/unix VARIANT=coverage submodules make ${MAKEOPTS} -C ports/unix VARIANT=coverage } |