Mirrors/servo
1
0
Fork 0
mirror of https://github.com/servo/servo.git synced 2025-06-06 16:45:39 +00:00
Code Issues Projects Releases Packages Wiki Activity

Auto merge of #19920 - servo:jdm-patch-10, r=aneeshusa

Browse source 
Supress output from git push in WPT sync.

Pushing to the remote exposes sensitive data in the logs of the job. The old token has been revoked as a consequence.

<!-- 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/19920)
<!-- Reviewable:end -->
This commit is contained in:
bors-servo 2018-02-01 18:09:55 -05:00 • committed by GitHub
commit b5e5a99cb7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -94,7 +94,7 @@ function unsafe_open_pull_request() {
AUTH="${WPT_SYNC_USER}:${WPT_SYNC_TOKEN}"
UPSTREAM="https://${AUTH}@github.com/${WPT_SYNC_USER}/servo.git"
git remote add "${REMOTE_NAME}" "${UPSTREAM}" || return 2
git push -f "${REMOTE_NAME}" "${BRANCH_NAME}" || return 3
git push -f "${REMOTE_NAME}" "${BRANCH_NAME}" &>/dev/null || return 3
# Prepare the pull request metadata.
BODY=":warning: Do not merge this PR without verifying that it "