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

Documentation/dev-release.txt

@@ -145,6 +145,12 @@ Commit the changes and create the release tag on the new commit:
   git tag -a v2.5
 ----
 
+Tag the plugins:
+
+----
+  git submodule foreach git tag -a v2.5
+----
+
 [[build-gerrit]]
 === Build Gerrit
 
@@ -313,20 +319,18 @@ get them merged
 [[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