Have the miri cronjob link to the failed run.
Also explain what needs to be done.
This commit is contained in:
parent
737319717c
commit
fed01ee814
1 changed files with 6 additions and 1 deletions
7
src/tools/miri/.github/workflows/ci.yml
vendored
7
src/tools/miri/.github/workflows/ci.yml
vendored
|
|
@ -174,7 +174,12 @@ jobs:
|
|||
~/.local/bin/zulip-send --stream miri --subject "Cron Job Failure (miri, $(date -u +%Y-%m))" \
|
||||
--message 'Dear @*T-miri*,
|
||||
|
||||
It would appear that the Miri cron job build failed. Would you mind investigating this issue?
|
||||
It would appear that the [Miri cron job build](https://github.com/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID) failed.
|
||||
|
||||
This likely means that rustc changed the miri directory and
|
||||
we now need to do a [`./miri rustc-pull`](https://github.com/rust-lang/miri/blob/master/CONTRIBUTING.md#importing-changes-from-the-rustc-repo).
|
||||
|
||||
Would you mind investigating this issue?
|
||||
|
||||
Thanks in advance!
|
||||
Sincerely,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue