| Age | Commit message (Collapse) | Author |
|---|
|
|
|
h/t SkySkimmer at
https://github.com/coq/coq/pull/12316#issuecomment-630952659
|
|
As per PR review request
|
|
Fixes #12300
Note that I currently only paginate the API call for the number of
reviews, not the main API call, because (a) the main API call doesn't
seem subject to pagination (it returns a dict, not an array), and (b)
because fetching the total number of pages incurs an extra API call for
each one that we want to paginate, even if there is only one page. We
could work around (b) with a significantly more complicated
`curl_paginate` function which heuristically recognizes the end of the
header/beginning of the body, such as
```bash
curl_paginate() {
# as per https://developer.github.com/v3/guides/traversing-with-pagination/#changing-the-number-of-items-received, GitHub will never give us more than 100
url="$1?per_page=100"
# We need to process the header to get the pagination. We have two
# options:
#
# 1. We can make an extra API call at the beginning to get the total
# number of pages, search for a rel="last" link, and then loop
# over all the pages.
#
# 2. We can ask for the header info with every single curl request,
# search for a rel="next" link to follow to the next page, and
# then parse out the body from the header.
#
# Although (1) is simpler, we choose to do (2) to save an extra API
# call per invocation of curl.
while [ ! -z "${url}" ]; do
response="$(curl -si "${url}")"
# we search for something like 'link: <https://api.github.com/repositories/1377159/pulls/12129/reviews?page=2>; rel="next", <https://api.github.com/repositories/1377159/pulls/12129/reviews?page=2>; rel="last"' and take the first 'next' url
url="$(echo "${response}" | grep -m 1 -io '^link: .*>; rel="next"' | grep -o '<[^>]*>; rel="next"' | grep -o '<[^>]*>' | sed s'/[<>]//g')"
echo "Response: ${response}" >&2
echo "${response}" |
{
is_header="yes"
while read line; do
if [ "${is_header}" == "yes" ]; then
if echo "${line}" | grep -q '^\s*[\[{]'; then # we treat lines beginning with [ or { as the beginning of the response body
is_header="no"
echo "${line}"
fi
else
echo "${line}"
fi
done
}
done
}
```
|
|
|
|
|
|
The message was confusing and the prompt let one reviewer think the
merge script would take care of doing the pull, which it doesn't.
|
|
This removes spurious Ack-by lines
|
|
shell buffer
Reviewed-by: ejgallego
|
|
|
|
|
|
The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
|
|
It used to output duplicate trailers.
|
|
This produces a commit message like
~~~
Merge PR #9250: coqchk: fix check for kelim with functors
Reviewed-by: ppedrot
Ack-by: mattam92
~~~
|
|
|
|
[ci skip]
|
|
|
|
This fulfils Gaetan's wish.
|
|
In case the local branch is ahead of upstream, we only print
a warning because it could be that we are merging several
PRs in a row.
|
|
As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
|
|
This should solve Emilio's problem.
|
|
In case the push URL has been overriden to make it fetch-only.
|
|
|
|
|
|
The script now performs many more checks and reports errors in
a more intelligible way.
|
|
|
|
|
|
|
|
Was still relying on the existence of user-configured /pr/.
|
|
|
