diff --git a/src/Init/System/FilePath.lean b/src/Init/System/FilePath.lean index fab5c64d5c..3e8fba0ed9 100644 --- a/src/Init/System/FilePath.lean +++ b/src/Init/System/FilePath.lean @@ -52,4 +52,8 @@ match fname.revPosOf pathSeparator with | some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString end FilePath + +def mkFilePath (parts : List String) : String := +String.intercalate FilePath.pathSeparator.toString parts + end System diff --git a/tests/lean/run/parseCore.lean b/tests/lean/run/parseCore.lean index 1567a5c994..6697bcee08 100644 --- a/tests/lean/run/parseCore.lean +++ b/tests/lean/run/parseCore.lean @@ -2,7 +2,7 @@ import Init.Lean.Parser def test : IO Unit := do env ← Lean.mkEmptyEnvironment; -Lean.Parser.parseFile env ("../../../src/Init/Core.lean"); +Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]); IO.println "done" #eval test