Add PR number to dev build artifact

[mbien]

@ebarboni had the idea for that - makes it easier to distinguish the artifacts once downloaded

will use github.run_id when run without PR context

going to update the downloader script too assuming this works

[matthiasblaesing]

Looks good to me.

If I remember correctly we currently don't have actions that run independently of PRs, but what happens when github.event.pull_request is not set then? Will it blow or just result in the name dev-build_?

[mbien]

If I remember correctly we currently don't have actions that run independently of PRs, but what happens when github.event.pull_request is not set then? Will it blow or just result in the name dev-build_?

right. The dev-build step is currently only label-activated, this would mean that the code path would only run with PR context.

I could try something like this though to cover the "what if" scenario:
dev-build_${{github.event.pull_request.number || github.run_id}}