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