Support opening a pull request by number

[roblourens]

If I know that I want to see pull request 123, it would be helpful if I could just put in the number instead of looking for it in a list.

[auchenberg]

Maybe via a command?

[RMacfarlane]

roblourens Are you imagining this would just open the description page of the pull request, or change the tree view as well?

[roblourens]

Maybe both? But the PR can exist in multiple places in the tree, that might not be easy

[meaghanlewis]

It seems like we still need to decide on the user experience here. In today's team sync we talked about opening the PR overview page.

[rbuckton]

My current workaround is to add a custom query:

    "githubPullRequests.queries": [
        {
            "label": "Specific Pull Request",
            "query": "is:open 40350"
        }
    ],

I could see a GitHub Pull Requests: View Pull Request... that prompted for the PR ID and added an entry into the Pull Requests list with a context-menu item to remove it. With such a feature someone could also theoretically write a Chrome/Edge Extension that adds an "Open PR In VS Code" button to GitHub that could launch VS Code and show the PR.

[RikkiGibson]

I feel like it could be reasonable to introduce a "special" tree view entry at the top level which accepts text input. For example

• a PR number
• a PR url
• an ad-hoc query

CodeStream has a similar feature.