Add "ready-to-merge" and "delegated" label from comment

[Merged by Bors] - chore(*): more `since :=` in `deprecated` #43996

Sign in to view logs

Triggered via issue June 11, 2024 23:44

mathlib-bors[bot]

commented on #13735 a43df3c

Status Skipped

Total duration 3s

Artifacts –

add_label_from_comment.yml

on: issue_comment

Add ready-to-merge label

Add delegated label