Commit 2025-10-29 02:50 a2b14f1d

ci: fix concurrency group (#31032) Multiple build runs from the same PR don't seem to be getting canceled. There's a suspicious line break in the concurrency option which might be confusing GitHub and causing this. cf. #mathlib4 > github action bandwidth @ 💬.