Feature: kill a background process

[mattjbray]

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.)

[charlesetc]

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!