make release optional

lean-dojo · Dec 25, 2024 · 2b0418e · 2b0418e
1 parent 0129cc5
commit 2b0418e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -118,14 +118,14 @@ private def nameToVersionedSharedLib (name : String) (v : String) : String :=
 
 def afterReleaseSync {α : Type} (pkg : Package) (build : SpawnM (Job α)) : FetchM (Job α) := do
   if pkg.preferReleaseBuild ∧ pkg.name ≠ (← getRootPackage).name then
-    (← pkg.gitHubRelease.fetch).bindAsync fun _ _ => build
+    (← pkg.optGitHubRelease.fetch).bindAsync fun _ _ => build
   else
     build
 
 
 def afterReleaseAsync {α : Type} (pkg : Package) (build : JobM α) : FetchM (Job α) := do
   if pkg.preferReleaseBuild ∧ pkg.name ≠ (← getRootPackage).name then
-    (← pkg.gitHubRelease.fetch).bindSync fun _ _ => build
+    (← pkg.optGitHubRelease.fetch).bindSync fun _ _ => build
   else
     Job.async build