From 451d73fbe2cbb4b03e4a8c08d44074b53c669035 Mon Sep 17 00:00:00 2001 From: Tshepang Mbambo Date: Mon, 28 Apr 2025 06:49:13 +0200 Subject: [PATCH] use repo name in push pr title I found "Rustc dev guide subtree update awkward" --- src/doc/rustc-dev-guide/josh-sync/src/sync.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/doc/rustc-dev-guide/josh-sync/src/sync.rs b/src/doc/rustc-dev-guide/josh-sync/src/sync.rs index cd64be636703..41d96397faab 100644 --- a/src/doc/rustc-dev-guide/josh-sync/src/sync.rs +++ b/src/doc/rustc-dev-guide/josh-sync/src/sync.rs @@ -194,7 +194,7 @@ impl GitSync { ); println!( // Open PR with `subtree update` title to silence the `no-merges` triagebot check - " https://github.com/{UPSTREAM_REPO}/compare/{github_user}:{branch}?quick_pull=1&title=Rustc+dev+guide+subtree+update&body=r?+@ghost" + " https://github.com/{UPSTREAM_REPO}/compare/{github_user}:{branch}?quick_pull=1&title=rustc-dev-guide+subtree+update&body=r?+@ghost" ); drop(josh);