From baadb2eae07bc46efc6c1a17c288dca30927c470 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sat, 14 Jan 2023 12:54:25 +0000 Subject: [PATCH] Unfortunately, inserting this reference resets the numbered list. backed out for now. --- mps/procedure/pull-request-merge.rst | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/mps/procedure/pull-request-merge.rst b/mps/procedure/pull-request-merge.rst index 83d604ab4ac..feb2c92a23b 100644 --- a/mps/procedure/pull-request-merge.rst +++ b/mps/procedure/pull-request-merge.rst @@ -93,8 +93,6 @@ considering `2. Purpose`_. talk to them about the matter. *Do not start the merging procedure*. -.. _checked pull request build results from CI: - #. Does the branch, and its merge, build and pass tests? CI should have run builds of both the branch, and a *trial merge* @@ -247,7 +245,7 @@ These steps will only rarely need repeating. - the merge was non-trivial - there has been any rebasing (see step 7) - - you haven't `checked pull request build results from CI`_ + - there were failed or missing build results from CI then build and test the merge result locally if possible. For example:: @@ -266,7 +264,7 @@ These steps will only rarely need repeating. - the merge was non-trivial - there has been any rebasing (see step 7) - - you haven't `checked pull request build results from CI`_ + - there were failed or missing build results from CI then push the merge to a fresh branch in the `Ravenbrook MPS repo on GitHub`_ to trigger CI to build and testing on all target