Skip to content

Commit 320f668

Browse files
committed
try removing path: head to fix PR creation job
1 parent 648e6ed commit 320f668

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

.github/workflows/kani-metrics.yml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ jobs:
1717
- name: Checkout Repository
1818
uses: actions/checkout@v4
1919
with:
20-
path: head
2120
submodules: true
2221

2322
# The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
@@ -27,12 +26,11 @@ jobs:
2726
python-version: '3.x'
2827

2928
- name: Compute Kani Metrics
30-
run: head/scripts/run-kani.sh --run metrics --path ${{github.workspace}}/head
29+
run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
3130

3231
- name: Create Pull Request
3332
uses: peter-evans/create-pull-request@v7
3433
with:
35-
token: ${{ secrets.GITHUB_TOKEN }}
3634
commit-message: Update Kani metrics
3735
title: 'Update Kani Metrics'
3836
body: |

0 commit comments

Comments
 (0)