From 40d2c9946319716228b414e501e71b7f959e1619 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 26 Jun 2025 11:55:06 +0200 Subject: [PATCH] chore: ci: fixes to Grove workflow (#9012) --- .github/workflows/grove.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/grove.yml b/.github/workflows/grove.yml index d99cac9da8..b795dc65db 100644 --- a/.github/workflows/grove.yml +++ b/.github/workflows/grove.yml @@ -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' }}