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: