From 198d3103cd6d06c0cde367a30a44ddf7f76a3d64 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 11 Dec 2021 09:12:33 +0100 Subject: [PATCH] chore: CI: propagate prepare-*.sh errors --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8d6a4c0e41..d9a67add83 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -113,7 +113,7 @@ jobs: cd build OPTIONS=() [[ -z '${{ matrix.llvm-url }}' ]] || wget -q ${{ matrix.llvm-url }} - [[ -z '${{ matrix.prepare-llvm }}' ]] || eval "OPTIONS+=($(../${{ matrix.prepare-llvm }}))" + [[ -z '${{ matrix.prepare-llvm }}' ]] || (extra_opts="$(../${{ matrix.prepare-llvm }})" && eval "OPTIONS+=($extra_opts)") if [[ $GITHUB_EVENT_NAME == 'schedule' && -n '${{ matrix.release }}' && -n '${{ secrets.PUSH_NIGHTLY_TOKEN }}' ]]; then git remote add nightly https://foo:'${{ secrets.PUSH_NIGHTLY_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-nightly.git git fetch nightly --tags