fix: stdin := .null in IO.Process.output

This commit is contained in:
tydeu 2023-09-14 14:26:22 -04:00 committed by Sebastian Ullrich
parent 6bdfde7939
commit 99b78bcc23
2 changed files with 6 additions and 2 deletions

View file

@ -10,6 +10,7 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f
v4.3.0 (development in progress)
---------
* `IO.Process.output` no longer inherits the standard input of the caller.
* The derive handler for `DecidableEq` [now handles](https://github.com/leanprover/lean4/pull/2591) mutual inductive types.
* [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616).
* [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598).

View file

@ -638,9 +638,12 @@ structure Output where
stdout : String
stderr : String
/-- Run process to completion and capture output. -/
/--
Run process to completion and capture output.
The process does not inherit the standard input of the caller.
-/
def output (args : SpawnArgs) : IO Output := do
let child ← spawn { args with stdout := Stdio.piped, stderr := Stdio.piped }
let child ← spawn { args with stdout := .piped, stderr := .piped, stdin := .null }
let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
let stderr ← child.stderr.readToEnd
let exitCode ← child.wait