;tools: push: github remote was renamed to origin (for jj)

This commit is contained in:
Simon Michael 2024-10-24 11:10:25 -10:00
parent 50bf401ea6
commit a9a4fd2906

View File

@ -6,7 +6,7 @@ set -e
INTERVAL="${1:-10}"
LOCALBRANCH=master
REMOTE=github
REMOTE=origin
REMOTECIBRANCH=ci
REMOTEMAINBRANCH=master
NUMRUNS=3