From ab78c4ffcad8f837fe1bcd7ff437ea876bc42b79 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sun, 8 Jan 2023 09:40:55 +0000 Subject: [PATCH] Clarifying that you can use your existing repo. --- mps/procedure/pull-request-merge.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mps/procedure/pull-request-merge.rst b/mps/procedure/pull-request-merge.rst index 54f27be71d4..67e8615cd98 100644 --- a/mps/procedure/pull-request-merge.rst +++ b/mps/procedure/pull-request-merge.rst @@ -118,7 +118,8 @@ These steps will only rarely need repeating. #. Clone the Ravenbrook MPS GitHub repository and name the remote "github". This will give you access to Travis CI to build and test - the merge. :: + the merge. (If you're an MPS developer you can use your existing + repo.) :: git clone -o github git@github.com:Ravenbrook/mps.git