Gerwin Klein a4c80a6887 github: use PR number to distinguish pull requests ... ${{github.ref}} will resolve to the base branch of the PR, not the PR branch, so it is not useful for distinguishing PRs. The pull request number will do the job. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>		2022-02-01 14:49:38 +11:00
..
workflows	github: use PR number to distinguish pull requests	2022-02-01 14:49:38 +11:00