Zulip Chat Archive
Stream: general
Topic: nolint and style-exceptions
Yaël Dillies (Jun 01 2021 at 14:06):
This is very minor but @leanprover-community-bot mistakens the file it modifies (nolint.txt instead of style-exceptions.txt):
https://github.com/leanprover-community/mathlib/commit/272a930a1d70d76436c193638b5959af6fc0510b
Bryan Gin-ge Chen (Jun 01 2021 at 14:09):
(The commit message is set here.)
Last updated: Aug 03 2023 at 10:10 UTC