chore: fix targets example

leanprover · Jul 27, 2022 · 93693d7 · 93693d7
1 parent bfa94d5
commit 93693d7
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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