public void close_pid (Pid pid)
On some platforms, notably Windows, the Pid type represents a resource which must be closed to prevent resource leaking.
close_pid is provided for this purpose. It should be used on all platforms, even though it doesn't do anything under UNIX.
The process reference to close