From a9f79c6a5b11784bfe1bf5bd18dc48d63420cd14 Mon Sep 17 00:00:00 2001
From: Adam Spiers <stow@adamspiers.org>
Date: Sun, 20 Nov 2016 22:00:46 +0000
Subject: [PATCH] make sure release tags are also pushed to GitHub

---
 doc/HOWTO-RELEASE | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/HOWTO-RELEASE b/doc/HOWTO-RELEASE
index 7be57bb..a8763c8 100644
--- a/doc/HOWTO-RELEASE
+++ b/doc/HOWTO-RELEASE
@@ -62,10 +62,12 @@ Release procedure
 
     git tag -s $version -m "Release $version"
 
-- Push HEAD and tag to savannah
+- Push HEAD and tag to savannah and GitHub:
 
-    git push
-    git push --tags
+    git push savannah
+    git push --tags savannah
+    git push github
+    git push --tags github
 
 - Regenerate the documentation for the website: