Zulip Chat Archive

I think Github changed something that broke linkifiers to PRs like: #10000, #1. Linkifiers to issues still work: #161, #6
Since we have overwhelmingly more PRs than issues, can we change the linkifiers so that #n refers to .../pull/n and issue#n to .../issue/n?

Joscha Mennicken (Dec 09 2021 at 20:53):

Linking to .../pull/n seems to redirect to .../issues/n if n is an issue. It doesn't redirect in the other direction though.

Floris van Doorn (Dec 09 2021 at 22:37):

Even better!

Eric Rodriguez (Dec 09 2021 at 22:38):

well the other way round was the old behaviour - maybe this may be changed again...

Gabriel Ebner (Dec 10 2021 at 10:18):

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.

Gabriel Ebner (Dec 10 2021 at 10:20):

I hope that this is a just a frontend change which will be rolled back when they realize the amount of broken links.

Eric Wieser (Dec 10 2021 at 10:22):

Until they do, should we swap our linkifier to use pull/ rather than issues/?

Gabriel Ebner (Dec 10 2021 at 10:26):

With our luck, they revert the change and then the pull/1234 links to issues are broken again.

Eric Rodriguez (Dec 10 2021 at 10:31):

https://github.com/github/feedback/discussions/8623 I found some discussion about this, and it supposedly doesn't happen when you're not logged in... what?!