From 53d313c74c41c03e68d9223bcf054893d3e3e4c1 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 27 Feb 2022 17:23:21 +0100
Subject: [PATCH] chore: fix function name

---
 src/Lean/Util/Path.lean           | 4 ++--
 tests/pkg/user_attr_app/Main.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 5b2a04be12..f5c08c1e24 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -83,7 +83,7 @@ def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
 /--
 Initialize Lean's search path given Lean's system root and an initial search path.
 The system root can be obtained via `getBuildDir` (for internal use) or
-`findSysroot?` (for external users). -/
+`findSysroot` (for external users). -/
 def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit := do
   let sp := sp ++ (← addSearchPathFromEnv (← getBuiltinSearchPath leanSysroot))
   searchPathRef.set sp
@@ -146,7 +146,7 @@ def searchModuleNameOfFileName (fname : FilePath) (rootDirs : SearchPath) : IO (
   e.g. in the case of `elan`'s proxy binary.
   Users internal to Lean should use `Lean.getBuildDir` instead.
 -/
-def findSysroot? (lean := "lean") : IO FilePath := do
+def findSysroot (lean := "lean") : IO FilePath := do
   if let some root ← IO.getEnv "LEAN_SYSROOT" then
     return root
   let out ← IO.Process.run {
diff --git a/tests/pkg/user_attr_app/Main.lean b/tests/pkg/user_attr_app/Main.lean
index f6813143e0..bdf86de03c 100644
--- a/tests/pkg/user_attr_app/Main.lean
+++ b/tests/pkg/user_attr_app/Main.lean
@@ -12,5 +12,5 @@ def tst : MetaM Unit := do
 #eval tst
 
 unsafe def main : IO Unit := do
-  initSearchPath (← Lean.findSysroot?) ["build/lib"]
+  initSearchPath (← Lean.findSysroot) ["build/lib"]
   withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => pure ()