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: Feb 28 2026 at 14:05 UTC