Skip to content

Commit f01a946

Browse files
authored
missing space
1 parent 7aec41c commit f01a946

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

scripts/runLinter.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -180,7 +180,7 @@ unsafe def runLinterOnModule (cfg : LinterConfig) (module : Name) : IO Unit := d
180180
IO.println s!"-- Linting passed for {module}."
181181

182182
/--
183-
Usage: `runLinter [--update] [--trace | -v] [--no-build][Batteries.Data.Nat.Basic]...`
183+
Usage: `runLinter [--update] [--trace | -v] [--no-build] [Batteries.Data.Nat.Basic]...`
184184
185185
Runs the linters on all declarations in the given modules
186186
(or all root modules of Lake `lean_lib` and `lean_exe` default targets if no module is specified).

0 commit comments

Comments
 (0)