1
0
mirror of https://github.com/RIOT-OS/RIOT.git synced 2025-12-24 22:13:52 +01:00

Merge pull request #18595 from kaspar030/ci_improve_makefile_broken_handling

CI: improve makefile broken handling
This commit is contained in:
Marian Buschsieweke 2022-09-15 16:55:30 +02:00 committed by GitHub
commit 121d960d15
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -379,7 +379,7 @@ get_app_board_toolchain_pairs() {
local prefix="$*"
if [ "$boards" = makefile_broken ]; then
echo "$appdir makefile_broken"
echo "$0 error \"error: ${DWQ_WORKER}: get_supported_boards failed in $appdir\""
return
fi