dev-release: simplify the command for pushing tags
This is also a less error-prone variant as the same tag name doesn't
have to be repeated twice.
Change-Id: I3b4ab97ef03b7ac4d2044e887fcdd9b0898a8549
diff --git a/Documentation/dev-release.txt b/Documentation/dev-release.txt
index 6726f4a..24c4832 100644
--- a/Documentation/dev-release.txt
+++ b/Documentation/dev-release.txt
@@ -313,13 +313,13 @@
For an `RC`:
+
----
- git push gerrit-review refs/tags/v2.5-rc0:refs/tags/v2.5-rc0
+ git push gerrit-review tag v2.5-rc0
----
+
For a final `stable` release:
+
----
- git push gerrit-review refs/tags/v2.5:refs/tags/v2.5
+ git push gerrit-review tag v2.5
----
