diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean index e01f16a263..5b6c069231 100644 --- a/src/Init/Lean/Util/Path.lean +++ b/src/Init/Lean/Util/Path.lean @@ -55,7 +55,7 @@ match val with | some val => parseSearchPath val sp @[export lean_init_search_path] -def initSearchPath (path : Option String := "") : IO Unit := +def initSearchPath (path : Option String := none) : IO Unit := match path with | some path => parseSearchPath path >>= searchPathRef.set | none => do