File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 44 pull_request :
55 branches : ["main"]
66 push :
7- branches : ["main", "nightly"]
7+ branches : ["main", "nightly-testing "]
88 workflow_dispatch :
99
1010concurrency :
Original file line number Diff line number Diff line change 1- name : Update Nightly
1+ name : Update nightly-testing
22
33on :
44 schedule :
1313 - name : checkout
1414 uses : actions/checkout@v6
1515 with :
16- ref : nightly
16+ ref : nightly-testing
1717 token : ${{ secrets.UNICODE_BASIC_TOKEN }}
1818
1919 - name : install jq
4141 - name : commit and push
4242 run : |
4343 git commit -m "chore: update toolchain ${{ steps.toolchain-tag.outputs.lean_tag }}"
44- git push --force origin nightly
44+ git push --force origin nightly-testing
Original file line number Diff line number Diff line change 3333 run : |
3434 git config user.name "${{ github.actor }}"
3535 git config user.email "${{ github.actor_id}}+${{ github.actor }}@users.noreply.github.com"
36- git merge -X theirs origin/nightly
36+ git merge -X theirs origin/nightly-testing
3737 echo "leanprover/lean4:${{ steps.toolchain-tag.outputs.lean_tag }}" > lean-toolchain
3838
3939 - name : create pull request
You can’t perform that action at this time.
0 commit comments