Skip to content

Commit 71568ab

Browse files
committed
chore: fix build
1 parent faf6277 commit 71568ab

1 file changed

Lines changed: 13 additions & 2 deletions

File tree

Manual/BuildTools/Lake/CLI.lean

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -852,8 +852,10 @@ USAGE:
852852
By default, runs the package's configured lint driver. If `builtinLint` is
853853
set to `true` in the package configuration, builtin lints also run.
854854

855-
A lint driver can be configured by either setting the `lintDriver` package
856-
configuration option or by tagging a script or executable `@[lint_driver]`.
855+
Positional `MODULE` arguments narrow only the builtin lints; if omitted,
856+
the workspace's default target roots are used. The lint driver is invoked
857+
with `lintDriverArgs` from the package config plus any arguments after
858+
`--`; the `MODULE` list is not passed to it.
857859

858860
OPTIONS:
859861
--builtin-lint run builtin environment linters
@@ -863,6 +865,15 @@ OPTIONS:
863865
--lint-only <name> run only the specified builtin linter (repeatable)
864866
--force skip the up-to-date build check
865867

868+
A lint driver can be configured by either setting the `lintDriver` package
869+
configuration option or by tagging a script or executable `@[lint_driver]`.
870+
A definition in a dependency can be used as a lint driver by using the
871+
`<pkg>/<name>` syntax for the 'lintDriver' configuration option.
872+
873+
A script lint driver will be run with the package configuration's
874+
`lintDriverArgs` plus the CLI `args`. An executable lint driver will be
875+
built and then run like a script.
876+
866877
```
867878

868879
:::lake lint " [\"--\" args...]"

0 commit comments

Comments
 (0)