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: May 02 2025 at 03:31 UTC