# command, triggered by $server_pid being non-zero. The server sends its output
# to a different file. The variable $server_opts, if not empty, contains
# options to disable IPv4 or IPv6 if necessary.
# command, triggered by $server_pid being non-zero. The server sends its output
# to a different file. The variable $server_opts, if not empty, contains
# options to disable IPv4 or IPv6 if necessary.