Label New Contributors

[Merged by Bors] - feat: lint upon importing `Lake` in mathlib #15417

Sign in to view logs

Triggered via pull request June 14, 2024 17:18

mattrobball

synchronize #13836

MR-lint-lake-import

Status Success

Total duration 13s

Artifacts –

label_new_contributor.yml

on: pull_request

label-and-report-new-contributor