Maintainer merge (comment)

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

Sign in to view logs

Triggered via issue June 11, 2024 23:44

mathlib-bors[bot]

commented on #13735 a43df3c

Status Skipped

Total duration 2s

Artifacts –

maintainer_merge_comment.yml

on: issue_comment

Ping maintainers on Zulip