From a9a4fd290671bbb673c7fa9efed7b0a4b42824ba Mon Sep 17 00:00:00 2001
From: Simon Michael <simon@joyful.com>
Date: Thu, 24 Oct 2024 11:10:25 -1000
Subject: [PATCH] ;tools: push: github remote was renamed to origin (for jj)

---
 tools/push | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/push b/tools/push
index 8abf59c7b..2f2432828 100755
--- a/tools/push
+++ b/tools/push
@@ -6,7 +6,7 @@ set -e
 INTERVAL="${1:-10}"
 
 LOCALBRANCH=master
-REMOTE=github
+REMOTE=origin
 REMOTECIBRANCH=ci
 REMOTEMAINBRANCH=master
 NUMRUNS=3