Documentation

Batteries.Lean.IO.Process

Running external commands. #

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

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

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

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

      Equations
        Instances For