Use a release- prefix for the tag on master (#3986)

The `v<VERSION>` tags are already used by the `release` branch, so use `release-<VERSION>` for `master` to avoid conflicts
runtimeverification · Jul 17, 2024 · 5fdd57a · 5fdd57a
1 parent c93594b
commit 5fdd57a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.github/workflows/master.yml b/.github/workflows/master.yml
@@ -78,6 +78,6 @@ jobs:
           ./package/version.sh sub
           if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
             git push origin release
-            git tag "v$(cat package/version)" origin/master
-            git push origin "v$(cat package/version)"
+            git tag "release-$(cat package/version)" origin/master
+            git push origin "release-$(cat package/version)"
           fi