fix: add mkFilePath and try to fix Windows build
This commit is contained in:
parent
d02ff42ade
commit
b5eb64da3a
2 changed files with 5 additions and 1 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue