diff options
Diffstat (limited to 'doc/HOWTO-RELEASE')
| -rw-r--r-- | doc/HOWTO-RELEASE | 8 |
1 files 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: |