From 24a1ea7d94331c611e146df026cedc6ba34e85c5 Mon Sep 17 00:00:00 2001 From: Joscha Date: Wed, 2 Sep 2026 17:43:02 +0200 Subject: [PATCH] chore: tweak adaptation PR "waiting for CI" message --- .github/workflows/adaptation-pr.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/adaptation-pr.yml b/.github/workflows/adaptation-pr.yml index c3fe7a0a9770..11eef6b38b66 100644 --- a/.github/workflows/adaptation-pr.yml +++ b/.github/workflows/adaptation-pr.yml @@ -81,6 +81,7 @@ jobs: app-slug: ${{ steps.app-token.outputs.app-slug }} upstream-pr: ${{ github.event.pull_request.number }} upstream-ci-green: ${{ steps.toolchain.outputs.exists }} + upstream-ci-green-msg: The adaptation PR will be created or updated once the toolchain is available. downstream-repo: leanprover/downstream-lean4 downstream-clone: downstream override-toolchain: ${{ steps.toolchain.outputs.toolchain }}