From ab87f23af50da997fdfbac1270592da84373db91 Mon Sep 17 00:00:00 2001 From: Richard Brooksby Date: Tue, 10 Jan 2023 10:17:38 +0000 Subject: [PATCH] Adding reference to github branch protection rules. --- mps/procedure/pull-request-merge.rst | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/mps/procedure/pull-request-merge.rst b/mps/procedure/pull-request-merge.rst index 1d9dc117adc..f00d1d1d588 100644 --- a/mps/procedure/pull-request-merge.rst +++ b/mps/procedure/pull-request-merge.rst @@ -337,6 +337,14 @@ repository are intended to last forever. That is why they have This policy has persisted over decades through more than one SCM system, and will persist when Git has been replaced by the next one. +Note: `GitHub branch protection rules`_ are `enabled +`_ on the +`Ravenbrook MPS repo on GitHub`_ and should prevent deletion. + +.. _Ravenbrook MPS repo on GitHub: https://github.com/Ravenbrook/mps + +.. _GitHub branch protection rules: https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/defining-the-mergeability-of-pull-requests/about-protected-branches#require-linear-history + A. References -------------