git-tag-release: Push branch and new tag
commit2e0ac79bda362ab0cb22f7c60233bf28b10df474
authorOlly Betts <olly@survex.com>
Wed, 20 Jul 2022 03:30:13 +0000 (20 15:30 +1200)
committerOlly Betts <olly@survex.com>
Tue, 30 Aug 2022 03:28:22 +0000 (30 15:28 +1200)
tree8a0915a318f40cd129affe056e348937f68820f9
parent99cf5e2ce928d3afc44422740dec907dab56642b
git-tag-release: Push branch and new tag

Ask first, as it's hard to undo a mistake that's gone public!

(cherry picked from commit d0fc1d8e5036420365b159c84fe94a8dc38ba370)
xapian-maintainer-tools/git-tag-release