Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-08-06 22:15:33 +01:00
Code Issues Projects Releases Packages Wiki Activity

Make the syncing PR a bit harder to mess up.

Browse source
This commit is contained in:
Josh Matthews 2018-02-01 09:53:56 -05:00 • committed by GitHub
parent dcd13b857c
commit 910e9db277
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
etc/ci/update-wpt-checkout
View file

@ -97,12 +97,14 @@ function unsafe_open_pull_request() {
git push -f "${REMOTE_NAME}" "${BRANCH_NAME}" || return 3 git push -f "${REMOTE_NAME}" "${BRANCH_NAME}" || return 3
# Prepare the pull request metadata. # Prepare the pull request metadata.
BODY="Automated downstream sync of changes from upstream as of " BODY=":warning: Do not merge this PR without verifying that it "
BODY+="is not overwriting local changes to web-platform-tests. :warning:\n\n
BODY+="Automated downstream sync of changes from upstream as of "
BODY+="${CURRENT_DATE}.\n" BODY+="${CURRENT_DATE}.\n"
BODY+="[no-wpt-sync]" BODY+="[no-wpt-sync]"
cat <<EOF >prdata.json || return 4 cat <<EOF >prdata.json || return 4
{ {
"title": "Sync WPT with upstream (${CURRENT_DATE})", "title": "[WIP] Sync WPT with upstream (${CURRENT_DATE})",
"head": "${WPT_SYNC_USER}:${BRANCH_NAME}", "head": "${WPT_SYNC_USER}:${BRANCH_NAME}",
"base": "master", "base": "master",
"body": "${BODY}", "body": "${BODY}",