diff options
| author | Jakub Beránek <berykubik@gmail.com> | 2025-07-25 08:27:18 +0200 |
|---|---|---|
| committer | Jakub Beránek <berykubik@gmail.com> | 2025-07-25 08:27:18 +0200 |
| commit | 60b054533fb607d0fac9716c1a6b94e9efa3b7a5 (patch) | |
| tree | c2ddb6e38217172e57a1553fcf69cf016bbe0513 | |
| parent | 94f725f8d214c4143c0a5bf8802f6d250fb30b3d (diff) | |
| download | rust-60b054533fb607d0fac9716c1a6b94e9efa3b7a5.tar.gz rust-60b054533fb607d0fac9716c1a6b94e9efa3b7a5.zip | |
Fix cronjob Zulip message
| -rw-r--r-- | src/tools/miri/.github/workflows/ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tools/miri/.github/workflows/ci.yml b/src/tools/miri/.github/workflows/ci.yml index 9f74642f0f1..e2e81370c60 100644 --- a/src/tools/miri/.github/workflows/ci.yml +++ b/src/tools/miri/.github/workflows/ci.yml @@ -219,7 +219,7 @@ jobs: 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). + we now need to do a [`rustc-josh-sync pull`](https://github.com/rust-lang/miri/blob/master/CONTRIBUTING.md#importing-changes-from-the-rustc-repo). Would you mind investigating this issue? |