Skip to content

Add "ready-to-merge" and "delegated" label #15858

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

Add "ready-to-merge" and "delegated" label #15858

Annotations

1 warning

Add ready-to-merge or delegated label

succeeded Jan 14, 2025 in 6s
Set up job
2s
Find bors merge/delegate
0s
Check whether user is a mathlib admin
0s
Add ready-to-merge or delegated label
0s
Remove "awaiting-author"
0s
Set up Python
0s
Install dependencies
0s
Run actions/checkout@v4
2s
Run Zulip Emoji Merge Delegate Script
0s
Post Run actions/checkout@v4
0s
Complete job
0s