From fed01ee8141be3cd065132640f0c551544ecca5f Mon Sep 17 00:00:00 2001 From: Oli Scherer Date: Tue, 21 Mar 2023 08:30:47 +0000 Subject: [PATCH] Have the miri cronjob link to the failed run. Also explain what needs to be done. --- src/tools/miri/.github/workflows/ci.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/tools/miri/.github/workflows/ci.yml b/src/tools/miri/.github/workflows/ci.yml index b71f48e4644b..2d487cb8f09a 100644 --- a/src/tools/miri/.github/workflows/ci.yml +++ b/src/tools/miri/.github/workflows/ci.yml @@ -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,