From ffcf715f3060dd3640ad554cdabf2bf5f550f96e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 5 Nov 2021 13:53:17 -0400
Subject: [PATCH] refactor: allow `-h` between command and args

---
 Lake/Cli.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index 2c4d4c6cd5..d1179c350e 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -349,12 +349,13 @@ def processArgs : CliM PUnit := do
   | [] => IO.println usage
   | ["--version"] => IO.println uiVersionString
   | _ => -- normal CLI
-    processLeadingOptions
+    processLeadingOptions -- between `lake` and command
     if let some cmd ← takeArg? then
+      processLeadingOptions -- between command and args
       if (← getWantsHelp) then
         IO.println <| help cmd
       else
-        processOptions
+        processOptions -- after/intermixed with args
         command cmd
     else
       if (← getWantsHelp) then IO.println usage else error "expected command"