From 3431d934debac8a6ecc2f9e16f06291dc1ba55cb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 22 May 2020 17:08:56 +0200
Subject: [PATCH] fix: initSearchPath: use valid default value

---
 src/Init/Lean/Util/Path.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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