Skip to content

Commit 40d2c99

Browse files
authored
chore: ci: fixes to Grove workflow (#9012)
1 parent 2c60f1a commit 40d2c99

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

.github/workflows/grove.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ permissions:
1111
jobs:
1212
grove-build:
1313
runs-on: ubuntu-latest
14+
if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
1415

1516
steps:
1617
- name: Retrieve information about the original workflow
@@ -53,7 +54,7 @@ jobs:
5354
uses: TwoFx/grove-action/fetch-upstream@v0
5455
with:
5556
artifact-name: grove-invalidated-facts
56-
base-ref: ${{ steps.workflow-info.outputs.targetCommitSha }}
57+
base-ref: master
5758

5859
- name: Download toolchain for this commit
5960
if: ${{ steps.should-run.outputs.should-run == 'true' }}

0 commit comments

Comments
 (0)