Zulip Chat Archive
Stream: mathlib4
Topic: unusedArguments
Antoine Labelle (Jan 19 2023 at 16:53):
I noticed that mathport doesn't translate @[nolint unused_arguments] into @[nolint unusedArguments]. Is this easy to fix?
Last updated: May 02 2025 at 03:31 UTC