;dev: tools/push improvements

This commit is contained in:
Simon Michael 2022-12-11 11:52:01 -10:00
parent c50df8bee8
commit c0b63c14e9

View File

@ -10,22 +10,38 @@ REMOTECIBRANCH=simon
REMOTEMAINBRANCH=master REMOTEMAINBRANCH=master
NUMRUNS=3 NUMRUNS=3
NUMCOMMITS=5 NUMCOMMITS=5
CISTARTDELAY=10 # too short, and the script will try to push too early CISTARTDELAY=5 # between ci push and run start
MAINPUSHDELAY=5 # between run end and master push
ciwait() { gitlog() {
echo "waiting for CI to start..." REF=$1
sleep $CISTARTDELAY git log --format='%ad %h %s%d' --date=short -$NUMCOMMITS ${REF:+"$REF"}
gh run list -L$NUMRUNS }
echo "waiting for CI to finish..."
ciwatch "$INTERVAL" runlog() {
echo "latest runs are:"
gh run list -L$NUMRUNS gh run list -L$NUMRUNS
} }
ciwait() {
runlog
echo "waiting for CI to start..."
sleep $CISTARTDELAY
runlog
echo "waiting for CI to finish..."
ciwatch "$INTERVAL"
runlog
echo "waiting for master to notice CI success..."
sleep $MAINPUSHDELAY
}
echo "latest local commits are:"
gitlog
echo "force-pushing to github/$REMOTECIBRANCH" echo "force-pushing to github/$REMOTECIBRANCH"
git push -f github $LOCALBRANCH:$REMOTECIBRANCH git push -f github $LOCALBRANCH:$REMOTECIBRANCH
ciwait ciwait
echo "pushing to $REMOTEMAINBRANCH" echo "pushing to $REMOTEMAINBRANCH"
git push github $REMOTEMAINBRANCH git push github $REMOTEMAINBRANCH
echo "Latest commits on github/$REMOTEMAINBRANCH are now:" echo "latest commits on github/$REMOTEMAINBRANCH are:"
git log --format='%ad %h %s%d' --date=short -$NUMCOMMITS github/$REMOTEMAINBRANCH gitlog github/$REMOTEMAINBRANCH
echo "done" echo "done"