| commit | 63ff153ea2e26fd19d0637356526da8ab667d449 | [log] [tgz] |
|---|---|---|
| author | David Ostrovsky <david.ostrovsky@gmail.com> | Tue Apr 06 14:39:30 2021 +0000 |
| committer | Gerrit Code Review <noreply-gerritcodereview@google.com> | Tue Apr 06 14:39:30 2021 +0000 |
| tree | e0f1766335a0e77f816c040c80b23db05582d6e0 | |
| parent | 457cf2c4657ca43cba8bbc4ce6d78ca5f8a32692 [diff] | |
| parent | e45f4d1e93d1bfbe2b2367a2ec10335de53a6394 [diff] |
Merge "Exclude jgit module from git push tag operation"
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]]