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

Auto merge of #19926 - servo:jdm-patch-13, r=emilio

Browse source 
Make the syncing PR a bit harder to mess up.

While the system is in testing, it's best to err on the side of making the PRs harder to merge.

<!-- Reviewable:start -->
---
This change is [<img src="https://reviewable.io/review_button.svg" height="34" align="absmiddle" alt="Reviewable"/>](https://reviewable.io/reviews/servo/servo/19926)
<!-- Reviewable:end -->
This commit is contained in:
bors-servo 2018-02-01 12:04:55 -06:00 • committed by GitHub
commit b20f01f1de
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
# 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+="[no-wpt-sync]"
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}",
"base": "master",
"body": "${BODY}",