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

fix: leanpkg on Windows

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-30 14:13:05 +01:00
parent d58b02a0be
commit a7e89f6d7e
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Leanpkg.lean
View file

@ -37,11 +37,14 @@ def build (leanArgs : List String) : IO Unit := do
let manifest ← readManifest
let path ← configure
let leanArgs := (match manifest.timeout with | some t => ["-T", toString t] | none => []) ++ leanArgs
execCmd {
let mut spawnArgs := {
cmd := "leanmake"
cwd := manifest.effectivePath
args := #[s!"LEAN_OPTS={" ".intercalate leanArgs}", s!"LEAN_PATH={path}"]
}
if System.Platform.isWindows then
spawnArgs := { spawnArgs with cmd := "sh", args := #[s!"{← IO.appDir}\\{spawnArgs.cmd}"] ++ spawnArgs.args }
execCmd spawnArgs
def initGitignoreContents :=
"/build