diff options
| author | Ralf Jung <post@ralfj.de> | 2024-10-26 07:23:51 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2024-10-26 07:23:51 +0200 |
| commit | 3ff01dd908a804e58f571035b1822d681a855446 (patch) | |
| tree | 5609c169fce35d664059f85aef7fc87b85eaec27 | |
| parent | 3432b91bbc863f8cacbb417afcfc1c0960740d9e (diff) | |
| download | rust-3ff01dd908a804e58f571035b1822d681a855446.tar.gz rust-3ff01dd908a804e58f571035b1822d681a855446.zip | |
automatic PR: explain how to trigger CI
| -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 f3975ec7389..2e491319822 100644 --- a/src/tools/miri/.github/workflows/ci.yml +++ b/src/tools/miri/.github/workflows/ci.yml @@ -139,7 +139,7 @@ jobs: git push -u origin $BRANCH - name: Create Pull Request run: | - PR=$(gh pr create -B master --title 'Automatic Rustup' --body '') + PR=$(gh pr create -B master --title 'Automatic Rustup' --body 'Please close and re-open this PR to trigger CI, then enable auto-merge.') ~/.local/bin/zulip-send --user $ZULIP_BOT_EMAIL --api-key $ZULIP_API_TOKEN --site https://rust-lang.zulipchat.com \ --stream miri --subject "Miri Build Failure ($(date -u +%Y-%m))" \ --message "A PR doing a rustc-pull [has been automatically created]($PR) for your convenience." |
