.

leanprover-community · Oct 2, 2024 · cd20dae · cd20dae
1 parent 23c24c3
commit cd20dae
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/lakefile.lean b/lakefile.lean
@@ -80,7 +80,7 @@ def widgetJsAllTarget (pkg : Package) (isDev : Bool) : FetchM (BuildJob (Array F
   We must instead ensure that the cloud release is fetched first
   so that this target does not build from scratch unnecessarily.
   `afterReleaseAsync` guarantees this. -/
-  pkg.afterReleaseAsync $ deps.bindSync fun depInfo depTrace => do
+  pkg.afterBuildCacheAsync $ deps.bindSync fun depInfo depTrace => do
     let traceFile := buildDir / "js" / "lake.trace"
     let _ ← buildUnlessUpToDate? traceFile depTrace traceFile do
        /- HACK: Ensure that NPM modules are installed before building TypeScript,

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:nightly-2024-10-02