Open mattjbray opened 5 months ago
A common pattern in bash is to start a long-running process in the background, do something, then kill it:
foo & FOO_PID=$! # do other stuff kill $FOO_PID
It'd be nice to have an API for this. (Currently there is no way to get the PID of a background_process.)
background_process
Yes that would be great to have. I guess a val kill : 'a background_process -> unit or something along those lines. Thanks for bringing it up!
val kill : 'a background_process -> unit
A common pattern in bash is to start a long-running process in the background, do something, then kill it:
It'd be nice to have an API for this. (Currently there is no way to get the PID of a
background_process
.)