Document github.ref_name instead of .head_ref

head_ref is only available in pull requests. ref_name is also available on push.
voxpupuli · Mar 21, 2022 · 151b0d3 · 151b0d3
1 parent 1da427c
commit 151b0d3
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -96,7 +96,7 @@ name: CI
 on: pull_request
 
 concurrency:
-  group: ${{ github.head_ref }}
+  group: ${{ github.ref_name }}
   cancel-in-progress: true
 
 jobs:
@@ -126,7 +126,7 @@ name: CI
 on: pull_request
 
 concurrency:
-  group: ${{ github.head_ref }}
+  group: ${{ github.ref_name }}
   cancel-in-progress: true
 
 jobs:
@@ -205,7 +205,7 @@ name: CI
 on: pull_request
 
 concurrency:
-  group: ${{ github.head_ref }}
+  group: ${{ github.ref_name }}
   cancel-in-progress: true
 
 jobs: