max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: initSearchPath: use valid default value

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-22 17:08:56 +02:00
parent 52b9bb35ea
commit 3431d934de
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Util/Path.lean
View file

@ -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