File tree Expand file tree Collapse file tree 3 files changed +8
-151
lines changed Expand file tree Collapse file tree 3 files changed +8
-151
lines changed Original file line number Diff line number Diff line change @@ -10,8 +10,6 @@ concurrency:
1010
1111jobs :
1212 cancel :
13- if : ${{ !github.event.pull_request.merged }}
14-
1513 permissions :
1614 actions : write
1715 contents : read
2624
2725 steps :
2826 - name : Cancel active PR runs for ${{ matrix.workflow_id }}
27+ continue-on-error : true
2928 uses : actions/github-script@5c56fde4671bc2d3592fb0f2c5b5bab9ddae03b1
3029 with :
3130 script : |
5150 });
5251 }
5352 }
53+
Load Diff This file was deleted.
Original file line number Diff line number Diff line change 1010 schedule :
1111 # Run the workflow every night at 2:00 AM UTC.
1212 - cron : " 0 2 * * *"
13+ workflow_dispatch :
1314
1415jobs :
1516 mirror-to-barretenberg-repo :
1819 - name : Checkout
1920 uses : actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
2021 with :
22+ ref : next
2123 fetch-depth : 0
2224 token : ${{ secrets.AZTEC_BOT_GITHUB_TOKEN }}
2325 - name : Push to barretenberg repo
2729 git config --global user.email [email protected] 2830
2931 if ./scripts/git_subrepo.sh push $SUBREPO_PATH --branch=master; then
30- git fetch # in case a commit came after this
31- git rebase origin/master
32+ git fetch origin next
33+ git rebase origin/next
3234 git commit --amend -m "$(git log -1 --pretty=%B) [skip ci]"
33- git push
35+ # We rely on the fixup logic instead
36+ # git push origin next
3437 fi
3538
You can’t perform that action at this time.
0 commit comments