diff options
| author | Josh Matthews <josh@joshmatthews.net> | 2018-02-01 09:53:56 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-01 09:53:56 -0500 |
| commit | 910e9db27707a26c74c2d5899599872dd31a64ad (patch) | |
| tree | 2667e015780ed80f9c2540d196bd322daaacddad /etc/ci | |
| parent | dcd13b857cc5085dcec5047433637af3d9013920 (diff) | |
| download | servo-910e9db27707a26c74c2d5899599872dd31a64ad.tar.gz servo-910e9db27707a26c74c2d5899599872dd31a64ad.zip | |
Make the syncing PR a bit harder to mess up.
Diffstat (limited to 'etc/ci')
| -rwxr-xr-x | etc/ci/update-wpt-checkout | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/etc/ci/update-wpt-checkout b/etc/ci/update-wpt-checkout index 574be72e716..78450b910ac 100755 --- a/etc/ci/update-wpt-checkout +++ b/etc/ci/update-wpt-checkout @@ -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}", |