File tree Expand file tree Collapse file tree 1 file changed +6
-1
lines changed
src/tools/miri/.github/workflows Expand file tree Collapse file tree 1 file changed +6
-1
lines changed Original file line number Diff line number Diff line change @@ -174,7 +174,12 @@ jobs:
174
174
~/.local/bin/zulip-send --stream miri --subject "Cron Job Failure (miri, $(date -u +%Y-%m))" \
175
175
--message 'Dear @*T-miri*,
176
176
177
- It would appear that the Miri cron job build failed. Would you mind investigating this issue?
177
+ It would appear that the [Miri cron job build](https://github.com/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID) failed.
178
+
179
+ This likely means that rustc changed the miri directory and
180
+ 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).
181
+
182
+ Would you mind investigating this issue?
178
183
179
184
Thanks in advance!
180
185
Sincerely,
You can’t perform that action at this time.
0 commit comments