[Merged by Bors] - chore: update Mathlib dependencies 2024-10-18 #60496
Triggered via issue
October 18, 2024 21:47
leanprover-community-mathlib4-bot
Status
Success
Total duration
14s
Artifacts
–
add_label_from_comment.yml
on: issue_comment
Add ready-to-merge label
5s
Add delegated label
0s
Annotations
1 warning
|
Add ready-to-merge label
Unexpected input(s) 'repository', 'issue_number', 'labels', valid inputs are ['route', 'mediaType']
|