make sure release tags are also pushed to GitHub

aspiers · Nov 20, 2016 · a9f79c6 · a9f79c6
1 parent 17bbfb0
commit a9f79c6
Showing 1 changed file with 5 additions and 3 deletions.
diff --git 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: