From 65ea45b17ba597ace0d00f6465b7e3ffef5b69c4 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 26 Jun 2025 14:15:51 +0200 Subject: [PATCH] chore: ci: fixes to Grove workflow (#9014) --- .github/workflows/grove.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/grove.yml b/.github/workflows/grove.yml index e53da97148..9821b3aad6 100644 --- a/.github/workflows/grove.yml +++ b/.github/workflows/grove.yml @@ -51,7 +51,7 @@ jobs: - name: Fetch upstream invalidated facts if: ${{ steps.should-run.outputs.should-run == 'true' && steps.workflow-info.outputs.pullRequestNumber != '' }} id: fetch-upstream - uses: TwoFx/grove-action/fetch-upstream@v0.1 + uses: TwoFx/grove-action/fetch-upstream@v0.3 with: artifact-name: grove-invalidated-facts base-ref: master @@ -95,7 +95,7 @@ jobs: - name: Build if: ${{ steps.should-run.outputs.should-run == 'true' }} id: build - uses: TwoFx/grove-action/build@v0.1 + uses: TwoFx/grove-action/build@v0.3 with: project-path: doc/std/grove script-name: grove-stdlib @@ -103,6 +103,7 @@ jobs: comment-artifact-name: grove-comment toolchain-id: lean4 toolchain-path: artifacts/${{ steps.unpack-toolchain.outputs.lean-dir }} + project-ref: ${{ steps.workflow-info.outputs.sourceHeadSha }} # deploy-alias computes a URL component for the PR preview. This # is so we can have a stable name to use for feedback on draft @@ -152,7 +153,7 @@ jobs: header: preview-comment recreate: true message: | - [Grove](${{ steps.deploy-draft.outputs.deploy-url }}). + [Grove](${{ steps.deploy-draft.outputs.deploy-url }}) for revision ${{ steps.workflow-info.outputs.sourceHeadSha }}. ${{ steps.build.outputs.comment-text }} env: