[plt-scheme] Web server pid
Greetings.
Is there a straightforward way of finding the (PLT) web server's PID
('straightforward', here, in the sense of 'less nasty than grepping
`ps`')? It's the sort of thing I'd rather anticipate seeing in
the .../log file, or in a .../run.pid beside it, but there's nothing
there, nothing obvious in web-server/private/launch.ss, and no
mention of it that I can see in the web-server docs.
Alternatively (for this is the point), is there some command-line
alternative support for shutting down a particular server? Again,
there's nothing obvious sitting alongside plt-web-server-text.
Thanks for any pointers. Best wishes,
Norman
--
------------------------------------------------------------------------
----
Norman Gray / http://nxg.me.uk
eurovotech.org / University of Leicester, UK