Identify pull request builds from GitHub Actions with the PR number

[Calinou]

• Follow-up to Store and display custom Git branch name in version information #83445 (can be merged independently).

This makes it easier to go back to the pull request the build was made from. The build name is displayed in the Project Manager, editor About dialog and editor version tooltip (at the bottom of the editor). It's also copied within the Copy System Information text.

Preview

GitHub Actions build from a push

GitHub Actions build from a pull request

PR number is 11 in this example (I was testing on my fork).

[aaronfranke]

I think this is a good idea, and the code looks pretty simple. I believe it should not conflict with anything, as if users are overriding the build name in the CI scons command that will take priority over the export variable.

[akien-mga]

Thanks!