diff options
| author | Ralf Jung <post@ralfj.de> | 2022-09-01 15:20:05 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-09-01 15:20:05 +0200 |
| commit | e12962b4aa1c019982fa83cbfc05939e398e8c25 (patch) | |
| tree | b6b0b8272e16d15f6221e894e056f46a13b68262 | |
| parent | 0da5f76a92584b2af13d0382da41119c88bdb521 (diff) | |
| download | rust-e12962b4aa1c019982fa83cbfc05939e398e8c25.tar.gz rust-e12962b4aa1c019982fa83cbfc05939e398e8c25.zip | |
Zulip notifications: ping the Miri team
| -rw-r--r-- | .github/workflows/ci.yml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 95303a592c8..8193411f879 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -142,7 +142,7 @@ jobs: ZULIP_API_TOKEN: ${{ secrets.ZULIP_API_TOKEN }} run: | ~/.local/bin/zulip-send --stream miri --subject "Cron Job Failure (miri, $(date -u +%Y-%m))" \ - --message 'Dear @**RalfJ** and @**oli** + --message 'Dear @*T-miri*, It would appear that the Miri cron job build failed. Would you mind investigating this issue? |