From a7e89f6d7eba87730aaa74f7d7e55fd875223e50 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 30 Dec 2020 14:13:05 +0100 Subject: [PATCH] fix: leanpkg on Windows --- src/Leanpkg.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean index e13d51a879..78ee3a8fde 100644 --- a/src/Leanpkg.lean +++ b/src/Leanpkg.lean @@ -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