Use pagination in fetching the number of reviews
Use pagination in fetching the number of reviews

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
}
```

gares/coq,ejgallego/coq,ejgallego/coq,coq/coq,JasonGross/coq,gares/coq,coq/coq,SkySkimmer/coq,gares/coq,ejgallego/coq,silene/coq,coq/coq,Zimmi48/coq,coq/coq,Zimmi48/coq,silene/coq,gares/coq,JasonGross/coq,SkySkimmer/coq,SkySkimmer/coq,JasonGross/coq,silene/coq,Zimmi48/coq,SkySkimmer/coq,gares/coq,Zimmi48/coq,ejgallego/coq,JasonGross/coq