commit e45f4d1e93d1bfbe2b2367a2ec10335de53a6394
author David Ostrovsky <david@ostrovsky.org> Tue Apr 06 00:23:19 2021 +0200
committer David Ostrovsky <david@ostrovsky.org> Tue Apr 06 12:50:28 2021 +0200
tree 9a0f0119cb2d2fa318f53e25bce2b6d903d4c22a
parent d5b9b141af6e2dff9c0cdea1a14cb68b608990eb

Exclude jgit module from git push tag operation

Change-Id: I58e430b736cff8a390162f2f8a204d7a5f0c7b88

Documentation/dev-release.txt

diff --git a/Documentation/dev-release.txt b/Documentation/dev-release.txt
index 736ccb0..0849c56 100644
--- a/Documentation/dev-release.txt
+++ b/Documentation/dev-release.txt
@@ -324,7 +324,7 @@
 Push the new Release Tag on the plugins:
 
 ----
-  git submodule foreach git push gerrit-review tag v$version
+  git submodule foreach '[ "$sm_path" == "modules/jgit" ] || git push gerrit-review tag "v$version"'
 ----
 
 [[upload-documentation]]