Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-08-03 20:50:07 +01:00
Code Issues Projects Releases Packages Wiki Activity

Auto merge of #29042 - servo:sync-perms, r=jdm

Browse source 
Work around WPT sync permission errors

Getting the permissions right to push the synced changes to servo-wpt-sync/servo and then open a PR was a bit of a nightmare. Instead, we can just push to a new branch on servo/servo and open the PR from there. Fixes #28920.
This commit is contained in:
bors-servo 2022-11-09 11:45:23 -05:00 • committed by GitHub
commit ace9b32b1c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

7
.github/workflows/wpt-nightly.yml vendored
View file

@ -122,9 +122,7 @@ jobs:
- name: Push changes - name: Push changes
uses: ad-m/github-push-action@master uses: ad-m/github-push-action@master
with: with:
github_token: ${{ secrets.GITHUB_TOKEN }}
branch: wpt_update_${{ env.CURRENT_DATE }} branch: wpt_update_${{ env.CURRENT_DATE }}
repository: servo-wpt-sync/servo
- name: Open PR - name: Open PR
env: env:
GH_TOKEN: ${{ secrets.WPT_SYNC_TOKEN }} GH_TOKEN: ${{ secrets.WPT_SYNC_TOKEN }}
@ -136,8 +134,5 @@ jobs:
r? @servo-wpt-sync r? @servo-wpt-sync
EOF EOF
) )
git remote add sync-fork https://github.com/servo-wpt-sync/servo.git
git fetch sync-fork ${{ env.UPDATE_BRANCH }}
git checkout ${{ env.UPDATE_BRANCH }}
# TODO: comment `@bors-servo r+` from `@servo-wpt-sync` # TODO: comment `@bors-servo r+` from `@servo-wpt-sync`
gh pr create --title "Sync WPT with upstream (${{ env.CURRENT_DATE }})" --body "$BODY" gh pr create --title "Sync WPT with upstream (${{ env.CURRENT_DATE }})" --body "$BODY" --head ${{ env.UPDATE_BRANCH }}