Skip to content

[Merged by Bors] - chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs #13568

[Merged by Bors] - chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs

[Merged by Bors] - chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs #13568

Triggered via issue January 7, 2025 17:41
Status Success
Total duration 11s
Artifacts

maintainer_bors.yml

on: issue_comment
Add ready-to-merge or delegated label
3s
Add ready-to-merge or delegated label
Fit to window
Zoom out
Zoom in

Annotations

1 warning
Add ready-to-merge or delegated label
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636