Skip to content

[#14999] chore: tweak adaptation PR "waiting for CI" message - #34

Merged
downstream-lean4[bot] merged 3 commits into
masterfrom
adaptation-14999
Sep 4, 2026
Merged

[#14999] chore: tweak adaptation PR "waiting for CI" message#34
downstream-lean4[bot] merged 3 commits into
masterfrom
adaptation-14999

Commits

Commits on Sep 2, 2026

Commits on Sep 3, 2026

Commits on Sep 4, 2026