We have to push the changes *and* the tags

diff --git a/do-release.sh b/do-release.sh
index 8e41665f15b672f82c5621b650e70d3c175920de..bf4824918ffc081b3132fbe74ec421407de34512 100755 (executable)
--- a/do-release.sh
+++ b/do-release.sh
@@ -65,5 +65,5 @@ git commit -a -m "Release version ${NEW_VERSION} generated by do-release.sh"
 git tag -a v${NEW_VERSION} -m "Version ${NEW_VERSION} release"
 
 echo -e ''
-echo -e '\033[37m\033[1mFinished.  Remember to git push --tags\033[0m'
+echo -e '\033[37mFinished.  Remember to \033[7mgit push\033[0m and then \033[7mgit push --tags\033[0m'
 echo -e ''