From 8bfde51ae895689e7bc237475e08f920049813d9 Mon Sep 17 00:00:00 2001 From: Simon Michael Date: Wed, 18 Oct 2023 13:33:12 +0100 Subject: [PATCH] ;dev:ci: rename usual CI branch to "ci" --- .github/workflows/ci.yml | 6 +++--- tools/push | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7738643d3..f5646d972 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -13,12 +13,12 @@ on: # schedule: # - cron: "0 07 * * 0" # sunday midnight pacific - # When there's a push to any of these dev branches, it runs in the dev branch. + # When there's a push to the ci branch, it runs there. # After passing there it can be merged/pushed to master. - # (Don't use these branches for pull requests, or it will run twice: + # (Don't use these branches for pull requests, or it will run twice, # https://github.community/t/how-to-trigger-an-action-on-push-or-pull-request-but-not-both/16662/2) push: - branches: [ simon, simon2 ] + branches: [ ci ] # When there's a pull request against master, it runs in the PR branch. # After passing there it can be merged/pushed to master. diff --git a/tools/push b/tools/push index f53427a9b..8abf59c7b 100755 --- a/tools/push +++ b/tools/push @@ -7,7 +7,7 @@ INTERVAL="${1:-10}" LOCALBRANCH=master REMOTE=github -REMOTECIBRANCH=simon +REMOTECIBRANCH=ci REMOTEMAINBRANCH=master NUMRUNS=3 NUMCOMMITS=5