From 855b1a37099438b7e278bb46a02ffb6555cb0b0e Mon Sep 17 00:00:00 2001
From: Kitamado <47292598+Seasawher@users.noreply.github.com>
Date: Sat, 23 Mar 2024 10:53:35 +0900
Subject: [PATCH] bug fix: invalid runCmd arguments

---
 lakefile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index ccfab51..4a50e87 100644
--- 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