Key the doc build concurrency group on the pull request number

[albertvillanova]

What does this PR do?

build_pr_documentation.yml keys its concurrency group on github.head_ref, which is the head branch name without the fork owner. Two open PRs from different forks whose branches share a name therefore land in the same group, and a push on one cancels the in-flight doc build on the other.

Shared names are common, because many contributors push to their fork's default branch instead of creating one: 8 of the 140 currently open PRs here already share a head branch name, all of them on main. A doc build takes around 3 minutes, which is the window in which such a collision cancels a build. I did not find a realized cancellation in the 100 most recent runs, so this is hardening rather than a fix for something currently failing.

github.event.pull_request.number is unique per pull request. This workflow only triggers on pull_request, so the github.run_id fallback is never reached, but keeping it means that a later trigger would fall back to never cancelling rather than to grouping by branch name.

The template this workflow was copied from carries the same expression, and the same one-liner is proposed there in huggingface/doc-builder#829.

[HuggingFaceDocBuilderDev]

The docs for this PR live here. All of your documentation changes will be reflected on that endpoint. The docs are available until 30 days after the last update.