fix: runCmd invalid arguments

lean-ja · Mar 23, 2024 · 2ba6f4f · 2ba6f4f
1 parent b6c86cb
commit 2ba6f4f
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -32,8 +32,8 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   return hasError
 
 script build do
-  if ← runCmd "lake exe mk_exercise" #["Src", "build"] then return 1
-  if ← runCmd "lake exe mdgen" #["build", "md/build"] then return 1
-  if ← runCmd "lake exe import_all" #["Src"] then return 1
-  if ← runCmd "mdbook build" #[] then return 1
+  if ← runCmd "lake" #["exe", "mk_exercise", "Src", "build"] then return 1
+  if ← runCmd "lake" #["exe", "mdgen", "build", "md/build"] then return 1
+  if ← runCmd "lake" #["exe", "import_all", "Src"] then return 1
+  if ← runCmd "mdbook" #["build"] then return 1
   return 0