You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It would appear that the [Miri cron job build](https://github.com/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID) failed.
177
+
It would appear that the [Miri cron job build]('"https://github.com/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"') failed.
178
178
179
179
This likely means that rustc changed the miri directory and
180
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).
0 commit comments