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: Dec 20 2023 at 11:08 UTC