From 53e757aea9f0fc537e28e39cf770fd40b67a81e9 Mon Sep 17 00:00:00 2001
From: Nick Craig-Wood <nick@craig-wood.com>
Date: Wed, 15 Mar 2023 13:34:30 +0000
Subject: [PATCH] build: update release docs to be more careful with the tag

---
 RELEASE.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/RELEASE.md b/RELEASE.md
index c2a23c277..7883ec696 100644
--- a/RELEASE.md
+++ b/RELEASE.md
@@ -10,7 +10,7 @@ This file describes how to make the various kinds of releases
 ## Making a release
 
   * git checkout master # see below for stable branch
-  * git pull
+  * git pull # IMPORTANT
   * git status - make sure everything is checked in
   * Check GitHub actions build for master is Green
   * make test # see integration test server or run locally
@@ -21,6 +21,7 @@ This file describes how to make the various kinds of releases
   * git status - to check for new man pages - git add them
   * git commit -a -v -m "Version v1.XX.0"
   * make retag
+  * git push origin # without --follow-tags so it doesn't push the tag if it fails
   * git push --follow-tags origin
   * # Wait for the GitHub builds to complete then...
   * make fetch_binaries