Two pages refer to `refs/pulls/NUM/head` instead of `refs/pull/NUM/head`

[jmarshall]

Code of Conduct

• I have read and agree to the GitHub Docs project's Code of Conduct

What article on docs.github.com is affected?

content/code-security/code-scanning/using-codeql-code-scanning-with-your-existing-ci-system/configuring-codeql-cli-in-your-ci-system.md

content/code-security/code-scanning/using-codeql-code-scanning-with-your-existing-ci-system/migrating-from-the-codeql-runner-to-codeql-cli.md

What part(s) of the article would you like to see updated?

These sections of these two pages refer to Git refs named refs/pulls/<PR-NUMBER>/xyz:

For the head commit of a pull request, use refs/pulls/NUMBER/head. For a GitHub-generated merge commit of a pull request, use refs/pulls/NUMBER/merge.

However all other documentation pages refer to similar refs as refs/pull/NUMBER/head (respectively …/merge) with …/pull/… singular. In extant repositories, it appears that refs/pull/NUMBER/xyz exists while refs/pulls/NUMBER/xyz does not.

Unless these two pages are confusingly referring to something else (e.g., a REST API call), it would appear that these instances of refs/pulls/… are incorrect.

[ramyaparimi]

@jmarshall
Thanks so much for opening an issue! I'll triage this for the team to take a look 👀

[felicitymay]

@jmarshall - many thanks for raising this issue. It sounds as if your assessment is right, but I'll double-check.

[jmarshall]

Thanks. While you've got the attention of people who know about these Git refs, please feel free to also direct their attention towards community/community#11922 😄 — which is what I was composing when I came across this small issue.

[felicitymay]

Unfortunately, I was talking to a different team 😞, but I'm sure that the team responsible for pull requests will do their best to respond to your feedback in a timely manner.

I've confirmed your assessment that refs/pulls is a typo. Would you like to raise a PR to fix this? Otherwise, I'll update the issue summary and add a help wanted label to this issue.

[jmarshall]

It might be more efficient for the docs team to just do it rather than review my attempt… Anyway, certainly there's no need for a help wanted request, so see PR #15817 which also fixes an unrelated minor typo I noticed a while back.

[felicitymay]

That's a good point. People who are new to GitHub often find it helpful to work on really small changes, like this one. So we have a tendency not to fix small issues but label them as good first issue (we have plenty of work in the mirrored internal repository keeping up with new features 🙂 ).

However, in this case the typo means that people have the wrong information to fulfil their task so getting it fixed quickly is great. Thanks for the PR 🙇🏻‍♀️