IO.Process.run that passes a String to stdin?

Stream: lean4

[Scott Morrison]

Does anyone have an example on hand of calling an external process and passing something (ideally a String!) to its stdin?

That is, I'd like something like IO.Process.run that also takes a string argument to pass to stdin, and return the string obtained from reading stdout.

[Scott Morrison]

Kyle pointed me to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/external.20process/near/345090183, which works perfectly.