From edea7ba9540b88a34e931ea33c8ffaa5cd486b6a Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Sun, 8 Jan 2023 08:19:34 +0000 Subject: [PATCH] Adding an option step to push to github promptly, and what to do if it doesn't happen automatically. --- mps/procedure/pull-request-merge.rst | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/mps/procedure/pull-request-merge.rst b/mps/procedure/pull-request-merge.rst index 2b79970e51d..b0d21a7b822 100644 --- a/mps/procedure/pull-request-merge.rst +++ b/mps/procedure/pull-request-merge.rst @@ -118,6 +118,10 @@ These steps will only rarely need repeating. `causes permanent pollution in the Ravenbrook Perforce repository `_. + [How does this affect the connection between the branch and the + pull request and issues? We want to retain that connection + forever. RB 2023-01-08] + 4. Optionally, let other people know that you're about to merge into master, and negotiate to avoid racing them to step 9 and making extra work for everyone. @@ -180,9 +184,23 @@ These steps will only rarely need repeating. git pull ravenbrook master -10. After a bit [how long? RB 2023-01-07] check that gitpushbot has - pushed the result to the Ravenbrook MPS repo on GitHub. [And do - what if it doesn't? RB 2023-01-07] +10. If and *only if* step 9 succeeds, you can optionally push to + GitHub:: + + git push github master branch/2023-01-06/speed-hax + + If you don't do this, then within `30 minutes + `_ + check that the merge appears in `the commits in the Ravenbrook MPS + repo on GitHub`_. + + If they do not appear: + + 1. Check email for error messages from gitpushbot and resolve them. + + 2. Check (or ask a sysadmin to check) that gitpushbot is running + on Berunda and restart it if necessary, or ask a sysadmin to do + this. 5. Rationale