;tools: push: select branch to push more robustly
This commit is contained in:
parent
1455a4d2fc
commit
7a5676dde4
@ -37,11 +37,11 @@ ciwait() {
|
|||||||
|
|
||||||
echo "latest local commits are:"
|
echo "latest local commits are:"
|
||||||
gitlog
|
gitlog
|
||||||
echo "force-pushing to github/$REMOTECIBRANCH"
|
echo "force-pushing $LOCALBRANCH to github/$REMOTECIBRANCH"
|
||||||
git push -f github $LOCALBRANCH:$REMOTECIBRANCH
|
git push -f github $LOCALBRANCH:$REMOTECIBRANCH
|
||||||
ciwait
|
ciwait
|
||||||
echo "pushing to $REMOTEMAINBRANCH"
|
echo "pushing CI-passing $LOCALBRANCH to $REMOTEMAINBRANCH"
|
||||||
git push github $REMOTEMAINBRANCH
|
git push github $LOCALBRANCH:$REMOTEMAINBRANCH
|
||||||
echo "latest commits on github/$REMOTEMAINBRANCH are:"
|
echo "latest commits on github/$REMOTEMAINBRANCH are:"
|
||||||
gitlog github/$REMOTEMAINBRANCH
|
gitlog github/$REMOTEMAINBRANCH
|
||||||
echo "done"
|
echo "done"
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user