Sigh. Mention that we have to do both a "git push" and a "git push --tags".

diff --git a/docs/README.developers b/docs/README.developers
index 5ab014abfe869979500d6fee9a14d3811f85eac8..ec0b29d7308528d4c791becc8fbf77e10f04d872 100644 (file)
--- a/docs/README.developers
+++ b/docs/README.developers
@@ -225,7 +225,9 @@ here; the convention for release candidates is to use something like
     convention here is to use VERSION+dev as the version number).
 
     % echo 1.5+dev > VERSION
-    % git commit VERSION; git push --tags
+    % git commit VERSION
+    % git push
+    % git push --tags
 
     Then do:
 
@@ -237,7 +239,7 @@ here; the convention for release candidates is to use something like
     % date +"%e %B %Y" > DATE
     (DATE should contain something like "30 December 2000")
 
- 3. % git commit VERSION DATE
+ 3. % git commit VERSION DATE; git push
 
  4. % git tag -a 1.5 -m 'Releasing nmh-1.5.'
     % git push --tags