Post PR summary comment

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

Sign in to view logs

Summary
Jobs
- build
Run details
- Usage
- Workflow file

Triggered via pull request June 14, 2024 17:18

mattrobball

synchronize #13836

MR-lint-lake-import

Status Success

Total duration 38s

Artifacts –

PR_summary.yml

on: pull_request