chore: report github actions failure on zulip (#4830)
only the master branch
This commit is contained in:
parent
39e0b41fe1
commit
d4f2db9559
1 changed files with 12 additions and 0 deletions
12
.github/workflows/ci.yml
vendored
12
.github/workflows/ci.yml
vendored
|
|
@ -455,12 +455,24 @@ jobs:
|
|||
# mark as merely cancelled not failed if builds are cancelled
|
||||
if: ${{ !cancelled() }}
|
||||
steps:
|
||||
- if: ${{ contains(needs.*.result, 'failure') && github.repository == 'leanprover/lean4' && github.ref_name == 'master' }}
|
||||
uses: zulip/github-actions-zulip/send-message@v1
|
||||
with:
|
||||
api-key: ${{ secrets.ZULIP_BOT_KEY }}
|
||||
email: "github-actions-bot@lean-fro.zulipchat.com"
|
||||
organization-url: "https://lean-fro.zulipchat.com"
|
||||
to: "infrastructure"
|
||||
topic: "Github actions"
|
||||
type: "stream"
|
||||
content: |
|
||||
A build of `${{ github.ref_name }}`, triggered by event `${{ github.event_name }}`, [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}).
|
||||
- if: contains(needs.*.result, 'failure')
|
||||
uses: actions/github-script@v7
|
||||
with:
|
||||
script: |
|
||||
core.setFailed('Some jobs failed')
|
||||
|
||||
|
||||
# This job creates releases from tags
|
||||
# (whether they are "unofficial" releases for experiments, or official releases when the tag is "v" followed by a semver string.)
|
||||
# We do not attempt to automatically construct a changelog here:
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue