From f92afee9b4bde3ed41017912eb93379cbfab0a82 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sun, 5 Sep 2021 19:47:13 -0400
Subject: [PATCH] fix: args bug with CLI

---
 Lake/Cli.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 2e89baf958..5da342fc0f 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -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