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