mirror of
https://github.com/danog/psalm.git
synced 2024-11-30 04:39:00 +01:00
Reorganize pushes to psalm/phar
Previously we built phar and pushed it: 1. To `psalm/phar:master` (always) 2. To `psalm/phar:$tag` (for tagged releases) However it's entirely possible to tag branches that diverged from master (like when we do a patch release for a legacy version). In this case our push to `psalm/phar:master` was rejected and script failed. As a result, `psalm/phar` was missing the tag (release). Now we will either: * push to `psalm/phar:master` (if the build was for `vimeo/psalm:master`) * or push to `psalm/phar:$tag` (if it's a tagged release)
This commit is contained in:
parent
59e549d2e8
commit
62e7e7f470
@ -23,12 +23,19 @@ git config user.email "github@muglug.com"
|
||||
git config user.name "Automated commit"
|
||||
git add --all .
|
||||
git commit -m "Updated Psalm phar to commit ${GITHUB_SHA}"
|
||||
git push origin master
|
||||
|
||||
tag=${GITHUB_REF/refs\/heads\//}
|
||||
tag=${tag/refs\/tags\//}
|
||||
|
||||
if [[ "$tag" != 'master' ]] ; then
|
||||
git tag "$tag"
|
||||
git push origin "$tag"
|
||||
fi
|
||||
|
||||
# this script runs on:
|
||||
# 1. pushes to master
|
||||
# 2. publishing releases
|
||||
#
|
||||
# So we push master to psalm/phar:master
|
||||
# and tags to psalm/phar:$tag
|
||||
|
||||
git push origin "$tag"
|
||||
|
Loading…
Reference in New Issue
Block a user