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

downstream: undo overrides

d85fb15
Select commit
Loading
Failed to load commit list.

Select a check to view from the sidebar