broken links

Stream: general

[Yury G. Kudryashov]

It looks like github no longer redirects from #10694 to https://github.com/leanprover-community/mathlib/pull/10694

[Kevin Buzzard]

The links both take me to the same place (on the Android app)

[Reid Barton]

I see the same behavior as Yury. Not :+1:ing the change, haha.

[Reid Barton]

Maybe it is in the process of being rolled out across different servers?

[Eric Wieser]

Might be worth contacting github support

[Kevin Buzzard]

I should perhaps say that both links are taking me from the Zulip app to the GitHub app on my phone

[Reid Barton]

I'm surprised I can't find any other information about this online

[Yury G. Kudryashov]

The app probably handles links using github API, not just visits the webpage.

[Gabriel Ebner]

(I've posted this in another stream here, for explanation I'm posting it here as well:) AFAIK github internally stored PRs as a special kind of issue. This is also visible in the REST API, where you get the PR comments using the issues/.../comments endpoints.

Note: GitHub's REST API v3 considers every pull request an issue, but not every issue is a pull request. For this reason, "Issues" endpoints may return both issues and pull requests in the response. You can identify pull requests by the pull_request key. Be aware that the id of a pull request returned from "Issues" endpoints will be an issue id. To find out the pull request id, use the "List pull requests" endpoint.