github: use correct label field

The trigger matched against the whole label object, not the name as
it should have.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2021-07-26 17:46:12 +10:00 committed by Gerwin Klein
parent f1ac3d829e
commit 4cdd97c532
2 changed files with 2 additions and 2 deletions

View file

@ -16,7 +16,7 @@ jobs:
# don't run again when other labels are added
if: ${{ github.event.action != 'labeled' &&
contains(github.event.pull_request.labels.*.name, 'proof-test') ||
github.event.action == 'labeled' && github.event.label == 'proof-test' }}
github.event.action == 'labeled' && github.event.label.name == 'proof-test' }}
strategy:
fail-fast: false
matrix:

View file

@ -48,7 +48,7 @@ jobs:
contains(github.event.pull_request.labels.*.name, 'hw-build') ||
github.event_name == 'pull_request' &&
github.event.action == 'labeled' &&
github.event.label == 'hw-build' }}
github.event.label.name == 'hw-build' }}
strategy:
fail-fast: false
matrix: