Merge pull request #74 from lean-dojo/peiyang

Fix lake monad bug
lean-dojo · May 25, 2024 · 62dfdc5 · 62dfdc5
2 parents 9b22717 + fde548a
commit 62dfdc5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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