dev-release: Document that plugins should also be tagged

Add commands for creating and pushing tags on the plugins.

Also remove the distinction between pushing final release and RC
release tags. This distinction is not made in the section about
creating the tags.

Change-Id: I4dcdc6ac81b2838b4fa9153efcecff87f3b07e3c
diff --git a/Documentation/dev-release.txt b/Documentation/dev-release.txt
index 2fe47a3..3d3104c 100644
--- a/Documentation/dev-release.txt
+++ b/Documentation/dev-release.txt
@@ -145,6 +145,12 @@
   git tag -a v2.5
 ----
 
+Tag the plugins:
+
+----
+  git submodule foreach git tag -a v2.5
+----
+
 [[build-gerrit]]
 === Build Gerrit
 
@@ -313,20 +319,18 @@
 [[push-tag]]
 ==== Push the Release Tag
 
-* Push the new Release Tag
-+
-For an `RC`:
-+
-----
-  git push gerrit-review tag v2.5-rc0
-----
-+
-For a final `stable` release:
-+
+Push the new Release Tag:
+
 ----
   git push gerrit-review tag v2.5
 ----
 
+Push the new Release Tag on the plugins:
+
+----
+  git submodule foreach git push gerrit-review tag v2.5
+----
+
 
 [[upload-documentation]]
 ==== Upload the Documentation