diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index 3b54130339..023295b0db 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -168,8 +168,8 @@ def helpScriptRun := USAGE: lake script run [[/]