From 93693d7ff6ef54f2e3e8e4315b54273a14b9f3ff Mon Sep 17 00:00:00 2001 From: tydeu Date: Wed, 27 Jul 2022 02:46:36 -0400 Subject: [PATCH] chore: fix targets example --- examples/targets/lakefile.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/targets/lakefile.lean b/examples/targets/lakefile.lean index a44d1a7..41ecdd0 100644 --- a/examples/targets/lakefile.lean +++ b/examples/targets/lakefile.lean @@ -17,11 +17,11 @@ lean_exe b lean_exe c @[defaultTarget] -target meow : PUnit := Target.opaqueSync (m := BuildM) do +target meow : PUnit := Target.mk <| sync (m := BuildM) do IO.FS.writeFile (_package.buildDir / "meow.txt") "Meow!" return default -target bark : PUnit := Target.opaqueSync (m := BuildM) do +target bark : PUnit := Target.mk <| sync (m := BuildM) do logInfo "Bark!" return default