Zulip Chat Archive
Stream: lean4
Topic: Passing options to `runLinter`
Michael Rothgang (Apr 06 2024 at 13:54):
Is there a way to pass additional options to runLinter, such as "also run this lint" or "only run that lint"? The --help output is very sparse.
Last updated: Dec 20 2025 at 21:32 UTC