Skip to content

[Merged by Bors] - feat: right-division as an OrderIso #65561

[Merged by Bors] - feat: right-division as an OrderIso

[Merged by Bors] - feat: right-division as an OrderIso #65561

Triggered via issue November 18, 2024 21:21
Status Success
Total duration 11s
Artifacts

add_label_from_comment.yml

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