From de1f95fa0da4994c700c080eb2dec2b692135ff8 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Fri, 13 Jan 2023 04:49:52 +0000 Subject: [PATCH] Adding example command for when the branch is already in the ravenbrook repo. --- mps/procedure/pull-request-merge.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mps/procedure/pull-request-merge.rst b/mps/procedure/pull-request-merge.rst index 2635a046085..ce9a31587a8 100644 --- a/mps/procedure/pull-request-merge.rst +++ b/mps/procedure/pull-request-merge.rst @@ -159,7 +159,9 @@ These steps will only rarely need repeating. If the pull request is from the `Ravenbrook MPS repo on GitHub`_, and its branch already has a conventional name, then use the - existing name. + existing name, e.g. :: + + git fetch github branch/2023-01-06/speed-hax:branch/2023-01-06/speed-hax If the branch to be merged is in a third-party repo, such as a fork not on GitHub, you can fetch it using a remote, e.g.::