From 26b1d510d9b5238d36b521d5367c707146fecd9d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sun, 5 Jan 2025 09:01:18 +1100
Subject: [PATCH] chore: bump toolchain to v4.16.0-rc1

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

diff --git a/lakefile.lean b/lakefile.lean
index b538ee0..2edab14 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -10,7 +10,7 @@ def srcNames := #["entity", "md4c", "md4c-html"]
 def wrapperName := "wrapper"
 def buildDir := defaultBuildDir
 
-def md4cOTarget (pkg : Package) (srcName : String) : FetchM (BuildJob FilePath) := do
+def md4cOTarget (pkg : Package) (srcName : String) : FetchM (Job FilePath) := do
   let oFile := pkg.dir / buildDir / md4cDir / ⟨ srcName ++ ".o" ⟩
   let srcTarget ← inputTextFile <| pkg.dir / md4cDir / ⟨ srcName ++ ".c" ⟩
   buildFileAfterDep oFile srcTarget fun srcFile => do
@@ -23,7 +23,7 @@ def md4cOTarget (pkg : Package) (srcName : String) : FetchM (BuildJob FilePath)
       let flags := #["-I", (pkg.dir / md4cDir).toString, "-fPIC"]
       compileO oFile srcFile flags
 
-def wrapperOTarget (pkg : Package) : FetchM (BuildJob FilePath) := do
+def wrapperOTarget (pkg : Package) : FetchM (Job FilePath) := do
   let oFile := pkg.dir / buildDir / wrapperDir / ⟨ wrapperName ++ ".o" ⟩
   let srcTarget ← inputTextFile <| pkg.dir / wrapperDir / ⟨ wrapperName ++ ".c" ⟩
   buildFileAfterDep oFile srcTarget fun srcFile => do
diff --git a/lean-toolchain b/lean-toolchain
index 57a4710..62ccd71 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.16.0-rc1