max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: args bug with CLI

Browse source
This commit is contained in:
tydeu 2021-09-05 19:47:13 -04:00
parent d6d395619f
commit f92afee9b4
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
Lake/Cli.lean
View file

@ -126,7 +126,6 @@ def processArgs : CliM PUnit := do
if (← getWantsHelp) then IO.println usage else
throw <| IO.userError "expected command"
| some cmd =>
let args ← collectArgs
if (← getWantsHelp) then IO.println (help cmd) else
command cmd