From cd20dae87c48495f0220663014dff11671597fcf Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 2 Oct 2024 20:24:38 +1000
Subject: [PATCH] .

---
 lakefile.lean  | 2 +-
 lean-toolchain | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lakefile.lean b/lakefile.lean
index ed03e87..e546225 100644
--- 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
index 8998520..e369dbe 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:nightly-2024-10-02