From 1b150ed05cde2f847dc5e6d62b799c46e827f499 Mon Sep 17 00:00:00 2001
From: Tshepang Mbambo <tshepang@gmail.com>
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"
---
 josh-sync/src/sync.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/josh-sync/src/sync.rs b/josh-sync/src/sync.rs
index cd64be636..41d96397f 100644
--- a/josh-sync/src/sync.rs
+++ b/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);