chore: ci: fixes to Grove workflow (#9012)

This commit is contained in:
Markus Himmel 2025-06-26 11:55:06 +02:00 committed by GitHub
parent 2c60f1a254
commit 40d2c99463
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -11,6 +11,7 @@ permissions:
jobs:
grove-build:
runs-on: ubuntu-latest
if: github.event.workflow_run.conclusion == 'success' && github.repository == 'leanprover/lean4'
steps:
- name: Retrieve information about the original workflow
@ -53,7 +54,7 @@ jobs:
uses: TwoFx/grove-action/fetch-upstream@v0
with:
artifact-name: grove-invalidated-facts
base-ref: ${{ steps.workflow-info.outputs.targetCommitSha }}
base-ref: master
- name: Download toolchain for this commit
if: ${{ steps.should-run.outputs.should-run == 'true' }}