From 7a5676dde4b2f21ee8917b46c12ea75eba8b4cfe Mon Sep 17 00:00:00 2001
From: Simon Michael <simon@joyful.com>
Date: Sat, 21 Jan 2023 09:54:49 -1000
Subject: [PATCH] ;tools: push: select branch to push more robustly

---
 tools/push | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tools/push b/tools/push
index fd7b16276..96eacab7c 100755
--- a/tools/push
+++ b/tools/push
@@ -37,11 +37,11 @@ ciwait() {
 
 echo "latest local commits are:"
 gitlog
-echo "force-pushing to github/$REMOTECIBRANCH"
+echo "force-pushing $LOCALBRANCH to github/$REMOTECIBRANCH"
 git push -f github $LOCALBRANCH:$REMOTECIBRANCH
 ciwait
-echo "pushing to $REMOTEMAINBRANCH"
-git push github $REMOTEMAINBRANCH
+echo "pushing CI-passing $LOCALBRANCH to $REMOTEMAINBRANCH"
+git push github $LOCALBRANCH:$REMOTEMAINBRANCH
 echo "latest commits on github/$REMOTEMAINBRANCH are:"
 gitlog github/$REMOTEMAINBRANCH
 echo "done"