Running external commands.

def IO.Process.runCmdWithInput' (cmd : String) (args : Array String) (input : String := "") (throwFailure : Bool := true) : IO Output

Pipe input into stdin of the spawned process, then return (exitCode, stdout, stdErr) upon completion.

Equations

• One or more equations did not get rendered due to their size.

def IO.Process.runCmdWithInput (cmd : String) (args : Array String) (input : String := "") (throwFailure : Bool := true) : IO String

Pipe input into stdin of the spawned process, then return the entire content of stdout as a String upon completion.

Equations

• IO.Process.runCmdWithInput cmd args input throwFailure = do let __do_lift ← IO.Process.runCmdWithInput' cmd args input throwFailure pure __do_lift.stdout