-
Brad King authored
We expect the server to exit when its communication pipes are closed. Close them and wait for the server to exit. If supported by the current version of python, kill the server if it does not exit after a few seconds.
d56f9237
A GitLab update will be applied on May 9th, between 8am and 10am, EDT (UTC-04:00). This site may have intermittent delays during that time.
We expect the server to exit when its communication pipes are closed. Close them and wait for the server to exit. If supported by the current version of python, kill the server if it does not exit after a few seconds.