Merge remote-tracking branch 'origin/master' into release

runtimeverification · Aug 10, 2024 · 74551b9 · 74551b9
2 parents 9fe0c97 + a29f783
commit 74551b9
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
@@ -18,6 +18,7 @@ jobs:
           # fetch-depth 0 means deep clone the repo
           fetch-depth: 0
           ref: ${{ github.event.pull_request.head.sha }}
+          token: ${{ secrets.JENKINS_GITHUB_PAT}}
       - name: 'Configure GitHub user'
         run: |
           git config user.name rv-jenkins