From 55356167253c83a749d99eebd0e171d9c802eb50 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 6 Mar 2022 16:48:49 +0100
Subject: [PATCH] chore: Bump toolchain

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

diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index d220389..e49f23b 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -16,7 +16,7 @@ def getLakePath : IO FilePath := do
   match (← IO.getEnv "LAKE") with
   | some path => pure $ System.FilePath.mk path
   | none =>
-    let lakePath := (←findSysroot?) / "bin" / "lake"
+    let lakePath := (←findSysroot) / "bin" / "lake"
     pure $ lakePath.withExtension System.FilePath.exeExtension
 
 -- Modified from the LSP Server
@@ -37,7 +37,7 @@ def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : I
     let stdout := stdout.split (· == '\n') |>.getLast!
     let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?)
       | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}"
-    initSearchPath (← findSysroot?) paths.oleanPath
+    initSearchPath (← findSysroot) paths.oleanPath
     paths.oleanPath.mapM realPathNormalized
   | 2 => pure []  -- no lakefile.lean
   | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}"
diff --git a/lean-toolchain b/lean-toolchain
index abadd14..8e380ba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-27
+leanprover/lean4:nightly-2022-03-06