;dev:ci: rename usual CI branch to "ci"

This commit is contained in:
Simon Michael 2023-10-18 13:33:12 +01:00
parent 6c95f47725
commit 8bfde51ae8
2 changed files with 4 additions and 4 deletions

View File

@ -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.

View File

@ -7,7 +7,7 @@ INTERVAL="${1:-10}"
LOCALBRANCH=master
REMOTE=github
REMOTECIBRANCH=simon
REMOTECIBRANCH=ci
REMOTEMAINBRANCH=master
NUMRUNS=3
NUMCOMMITS=5