Skip to content

[wip] [ci] doc-job-skip take #4.5 dry-run via github direct edit #8997

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
stas00 wants to merge 6 commits into from
Closed

[wip] [ci] doc-job-skip take #4.5 dry-run via github direct edit #8997

Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
57323e9
[wip] [ci] doc-job-skip take #4.5 dry-run via github direct edit
stas00 Dec 9, 2020
f7296d6
doc test
stas00 Dec 9, 2020
59ea3e4
Merge remote-tracking branch 'origin/master' into stas00-patch-1
stas00 Dec 10, 2020
321a6e4
use head's username
stas00 Dec 10, 2020
dc775bc
restore
stas00 Dec 10, 2020
8eacf1a
doc fix
stas00 Dec 10, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .circleci/config.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ commands:
then
echo $CIRCLE_PR_NUMBER
resp=$(curl -Ls https://api.github.com/repos/huggingface/transformers/pulls/${CIRCLE_PR_NUMBER})
user=$(jq -r .user.login \<<< $resp) # PR creator username
head_ref=$(jq -r .head.ref \<<< $resp) # PR user's branch name
user=$(jq -r .head.user.login \<<< $resp) # PR head username
head_ref=$(jq -r .head.ref \<<< $resp) # PR head branch name
echo head_ref=$head_ref, user=$user
fi

Expand Down