From fde548acb61bfef1ffef306b35a898d517c30ea1 Mon Sep 17 00:00:00 2001 From: Peiyang Song Date: Sat, 25 May 2024 15:56:03 -0700 Subject: [PATCH] Fix lake monad bug --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index 1e227d5..f34eaf9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -123,7 +123,7 @@ def afterReleaseSync {α : Type} (pkg : Package) (build : SpawnM (Job α)) : Fet build -def afterReleaseAsync {α : Type} (pkg : Package) (build : BuildM α) : FetchM (Job α) := do +def afterReleaseAsync {α : Type} (pkg : Package) (build : JobM α) : FetchM (Job α) := do if pkg.preferReleaseBuild ∧ pkg.name ≠ (← getRootPackage).name then (← pkg.release.fetch).bindSync fun _ _ => build else