bug fix: invalid runCmd arguments

leanprover-community · Mar 23, 2024 · 855b1a3 · 855b1a3
1 parent 5307ff3
commit 855b1a3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lakefile.lean b/lakefile.lean
@@ -22,5 +22,5 @@ def runCmd (cmd : String) (args : Array String) : ScriptM Bool := do
   return hasError
 
 script build do
-  if ← runCmd "lake exe mdgen" #["lean", "md"] then return 1
+  if ← runCmd "lake" #["exe", "mdgen", "lean", "md"] then return 1
   return 0