continuous integration (staging)

fix: silence the header linter on non-`Mathlib.lean` imported files (… #12114

Sign in to view logs

Run time

Learn about OS pricing on GitHub Actions

Job	Run time
Cancel Previous Runs (CI)	4s
Lint style	37s
Build	42m 20s
Post-CI job	11s
	43m 12s