chore: adaptations for lean4#5542 (#17564) #695
mathlib-bors[bot]add_label_from_diff.yaml
on: push
Add topic label
1m 0s
Annotations
1 warning and 1 notice
|
Add topic label
no label to add
|
|
Add topic label
Applicable labels: #[]
|