Gerwin Klein de4341adee github: use PR number instead of ref ... ${{github.ref}} is not what it seems for pull request target. It will point to the base branch instead of refs/pulls/<num> like the docs would suggest. Using the PR number directly should work. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>		2022-01-19 09:28:53 +11:00
..
workflows	github: use PR number instead of ref	2022-01-19 09:28:53 +11:00